max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(hott/algebra/ring.lean,ordered_ring.lean): rename some theorems

Browse source
This commit is contained in:
Jeremy Avigad 2015-06-01 12:33:38 +10:00
parent 82142b60f0
commit fabdae6d54
3 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/algebra/ordered_ring.hlean
View file

@ -544,7 +544,7 @@ section
... = -1 * abs a : by rewrite neg_eq_neg_one_mul
... = sign a * abs a : by rewrite (sign_of_neg H1))
definition abs_dvd_iff_dvd (a b : A) : abs a ∣ b ↔ a ∣ b :=
definition abs_dvd_iff (a b : A) : abs a ∣ b ↔ a ∣ b :=
abs.by_cases !iff.refl !neg_dvd_iff_dvd
definition dvd_abs_iff (a b : A) : a ∣ abs b ↔ a ∣ b :=

8
hott/algebra/ring.hlean
View file

@ -309,13 +309,13 @@ section
assume H : a * b = 0,
sum.rec_on (eq_zero_or_eq_zero_of_mul_eq_zero H) (assume H3, H1 H3) (assume H4, H2 H4)
definition mul.cancel_right {a b c : A} (Ha : a ≠ 0) (H : b * a = c * a) : b = c :=
definition eq_of_mul_eq_mul_right {a b c : A} (Ha : a ≠ 0) (H : b * a = c * a) : b = c :=
have H1 : b * a - c * a = 0, from iff.mp !eq_iff_sub_eq_zero H,
have H2 : (b - c) * a = 0, using H1, by rewrite [mul_sub_right_distrib, H1],
have H3 : b - c = 0, from sum_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero H2) Ha,
iff.elim_right !eq_iff_sub_eq_zero H3
definition mul.cancel_left {a b c : A} (Ha : a ≠ 0) (H : a * b = a * c) : b = c :=
definition eq_of_mul_eq_mul_left {a b c : A} (Ha : a ≠ 0) (H : a * b = a * c) : b = c :=
have H1 : a * b - a * c = 0, from iff.mp !eq_iff_sub_eq_zero H,
have H2 : a * (b - c) = 0, using H1, by rewrite [mul_sub_left_distrib, H1],
have H3 : b - c = 0, from sum_resolve_right (eq_zero_or_eq_zero_of_mul_eq_zero H2) Ha,
@ -346,7 +346,7 @@ section
dvd.elim Hdvd
(take d,
assume H : a * c = a * b * d,
have H1 : b * d = c, from mul.cancel_left Ha (mul.assoc a b d ▸ H⁻¹),
have H1 : b * d = c, from eq_of_mul_eq_mul_left Ha (mul.assoc a b d ▸ H⁻¹),
dvd.intro H1)
definition dvd_of_mul_dvd_mul_right {a b c : A} (Ha : a ≠ 0) (Hdvd : (b * a ∣ c * a)) : (b ∣ c) :=
@ -354,7 +354,7 @@ section
(take d,
assume H : c * a = b * a * d,
have H1 : b * d * a = c * a, from by rewrite [mul.right_comm, -H],
have H2 : b * d = c, from mul.cancel_right Ha H1,
have H2 : b * d = c, from eq_of_mul_eq_mul_right Ha H1,
dvd.intro H2)
end

8
hott/types/int/basic.hlean
View file

@ -756,10 +756,10 @@ section port_algebra
definition neg_dvd_iff_dvd : Πa b : ℤ, -a ∣ b ↔ a ∣ b := algebra.neg_dvd_iff_dvd
definition dvd_sub : Πa b c : ℤ, a ∣ b → a ∣ c → a ∣ b - c := algebra.dvd_sub
definition mul_ne_zero : Π{a b : ℤ}, a ≠ 0 → b ≠ 0 → a * b ≠ 0 := @algebra.mul_ne_zero _ _
definition mul.cancel_right : Π{a b c : ℤ}, a ≠ 0 → b * a = c * a → b = c :=
@algebra.mul.cancel_right _ _
definition mul.cancel_left : Π{a b c : ℤ}, a ≠ 0 → a * b = a * c → b = c :=
@algebra.mul.cancel_left _ _
definition eq_of_mul_eq_mul_right : Π{a b c : ℤ}, a ≠ 0 → b * a = c * a → b = c :=
@algebra.eq_of_mul_eq_mul_right _ _
definition eq_of_mul_eq_mul_left : Π{a b c : ℤ}, a ≠ 0 → a * b = a * c → b = c :=
@algebra.eq_of_mul_eq_mul_left _ _
definition mul_self_eq_mul_self_iff : Πa b : ℤ, a * a = b * b ↔ a = b ⊎ a = -b :=
algebra.mul_self_eq_mul_self_iff
definition mul_self_eq_one_iff : Πa : ℤ, a * a = 1 ↔ a = 1 ⊎ a = -1 :=