From d33c91d7b90496128a3f56c725a045043d673aca Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sat, 23 May 2015 14:05:06 +1000 Subject: [PATCH] fix({hott,library}/algebra/*): fix names --- hott/algebra/field.hlean | 17 +++++++---------- hott/algebra/group.hlean | 6 +++--- hott/algebra/ring.hlean | 2 +- library/algebra/field.lean | 17 +++++++---------- library/algebra/group.lean | 8 +++----- library/algebra/group_power.lean | 8 ++++---- library/algebra/ring.lean | 2 +- 7 files changed, 26 insertions(+), 34 deletions(-) diff --git a/hott/algebra/field.hlean b/hott/algebra/field.hlean index cef97927d..7c4049ef8 100644 --- a/hott/algebra/field.hlean +++ b/hott/algebra/field.hlean @@ -10,7 +10,6 @@ The development is modeled after Isabelle's library. Ported from the standard library -/ ----------------------------------------------------------------------------------------------------- import algebra.ring open core @@ -78,12 +77,11 @@ section division_ring -- definition ne_zero_of_one_div_ne_zero (H : 1 / a ≠ 0) : a ≠ 0 := -- assume Ha : a = 0, absurd (Ha⁻¹ ▸ one_div_zero) H - -- the analogue in group is called inv_one - definition inv_one_is_one : 1⁻¹ = (1:A) := + definition inv_one_eq : 1⁻¹ = (1:A) := by rewrite [-mul_one, (inv_mul_cancel (ne.symm zero_ne_one))] definition div_one : a / 1 = a := - by rewrite [↑divide, inv_one_is_one, mul_one] + by rewrite [↑divide, inv_one_eq, mul_one] definition zero_div : 0 / a = 0 := !zero_mul @@ -94,10 +92,9 @@ section division_ring absurd C1 Ha definition mul_ne_zero_comm (H : a * b ≠ 0) : b * a ≠ 0 := - have H2 : a ≠ 0 × b ≠ 0, from mul_ne_zero_imp_ne_zero H, + have H2 : a ≠ 0 × b ≠ 0, from ne_zero_and_ne_zero_of_mul_ne_zero H, mul_ne_zero' (prod.pr2 H2) (prod.pr1 H2) - -- make "left" and "right" versions? definition eq_one_div_of_mul_eq_one (H : a * b = 1) : b = 1 / a := have H2 : a ≠ 0, from @@ -169,7 +166,7 @@ section division_ring -- oops, the analogous definition in group is called inv_mul, but it *should* be called -- mul_inv, in which case, we will have to rename this one - definition mul_inv (Ha : a ≠ 0) (Hb : b ≠ 0) : (b * a)⁻¹ = a⁻¹ * b⁻¹ := + definition mul_inv_eq (Ha : a ≠ 0) (Hb : b ≠ 0) : (b * a)⁻¹ = a⁻¹ * b⁻¹ := have H1 : b * a ≠ 0, from mul_ne_zero' Hb Ha, inverse (calc a⁻¹ * b⁻¹ = (1 / a) * b⁻¹ : inv_eq_one_div @@ -236,7 +233,7 @@ section field by rewrite [(one_div_mul_one_div Ha Hb), mul.comm b] definition div_mul_right (Hb : b ≠ 0) (H : a * b ≠ 0) : a / (a * b) = 1 / b := - let Ha : a ≠ 0 := prod.pr1 (mul_ne_zero_imp_ne_zero H) in + let Ha : a ≠ 0 := prod.pr1 (ne_zero_and_ne_zero_of_mul_ne_zero H) in inverse (calc 1 / b = 1 * (1 / b) : one_mul ... = (a * a⁻¹) * (1 / b) : mul_inv_cancel Ha @@ -261,7 +258,7 @@ section field by rewrite [add.comm, -(div_mul_left Ha H), -(div_mul_right Hb H), ↑divide, -right_distrib] definition div_mul_div (Hb : b ≠ 0) (Hd : d ≠ 0) : (a / b) * (c / d) = (a * c) / (b * d) := - by rewrite [↑divide, 2 mul.assoc, (mul.comm b⁻¹), mul.assoc, (mul_inv Hd Hb)] + by rewrite [↑divide, 2 mul.assoc, (mul.comm b⁻¹), mul.assoc, (mul_inv_eq Hd Hb)] definition mul_div_mul_left (Hb : b ≠ 0) (Hc : c ≠ 0) : (c * a) / (c * b) = a / b := have H [visible] : c * b ≠ 0, from mul_ne_zero' Hc Hb, @@ -402,7 +399,7 @@ section discrete_field (assume Ha : a ≠ 0, decidable.by_cases (assume Hb : b = 0, by rewrite [Hb, zero_mul, 2 inv_zero, mul_zero]) - (assume Hb : b ≠ 0, mul_inv Ha Hb)) + (assume Hb : b ≠ 0, mul_inv_eq Ha Hb)) -- the following are specifically for fields definition one_div_mul_one_div''' : (1 / a) * (1 / b) = 1 / (a * b) := diff --git a/hott/algebra/group.hlean b/hott/algebra/group.hlean index 33b6b6733..e714f4ebd 100644 --- a/hott/algebra/group.hlean +++ b/hott/algebra/group.hlean @@ -166,7 +166,7 @@ section group theorem inv_eq_of_mul_eq_one {a b : A} (H : a * b = 1) : a⁻¹ = b := by rewrite [-mul_one a⁻¹, -H, inv_mul_cancel_left] - theorem inv_one : 1⁻¹ = (1:A) := inv_eq_of_mul_eq_one (one_mul 1) + theorem one_inv : 1⁻¹ = (1:A) := inv_eq_of_mul_eq_one (one_mul 1) theorem inv_inv (a : A) : (a⁻¹)⁻¹ = a := inv_eq_of_mul_eq_one (mul.left_inv a) @@ -177,7 +177,7 @@ section group iff.intro (assume H, inv.inj H) (assume H, ap _ H) theorem inv_eq_one_iff_eq_one (a b : A) : a⁻¹ = 1 ↔ a = 1 := - inv_one ▸ inv_eq_inv_iff_eq a 1 + one_inv ▸ inv_eq_inv_iff_eq a 1 theorem eq_inv_of_eq_inv {a b : A} (H : a = b⁻¹) : b = a⁻¹ := by rewrite [H, inv_inv] @@ -202,7 +202,7 @@ section group ... = a * 1 : mul.right_inv ... = a : mul_one - theorem inv_mul (a b : A) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := + theorem mul_inv (a b : A) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := inv_eq_of_mul_eq_one (calc a * b * (b⁻¹ * a⁻¹) = a * (b * (b⁻¹ * a⁻¹)) : mul.assoc diff --git a/hott/algebra/ring.hlean b/hott/algebra/ring.hlean index d42e95de2..b087d45a6 100644 --- a/hott/algebra/ring.hlean +++ b/hott/algebra/ring.hlean @@ -230,7 +230,7 @@ section ... = 0 : mul_zero, inverse (neg_eq_of_add_eq_zero H) - definition mul_ne_zero_imp_ne_zero {a b : A} (H : a * b ≠ 0) : a ≠ 0 × b ≠ 0 := + definition ne_zero_and_ne_zero_of_mul_ne_zero {a b : A} (H : a * b ≠ 0) : a ≠ 0 × b ≠ 0 := have Ha : a ≠ 0, from (assume Ha1 : a = 0, have H1 : a * b = 0, by rewrite [Ha1, zero_mul], diff --git a/library/algebra/field.lean b/library/algebra/field.lean index 87a1bd26d..6fa18d27c 100644 --- a/library/algebra/field.lean +++ b/library/algebra/field.lean @@ -76,12 +76,11 @@ section division_ring -- theorem ne_zero_of_one_div_ne_zero (H : 1 / a ≠ 0) : a ≠ 0 := -- assume Ha : a = 0, absurd (Ha⁻¹ ▸ one_div_zero) H - -- the analogue in group is called inv_one - theorem inv_one_is_one : 1⁻¹ = (1:A) := + theorem one_inv_eq : 1⁻¹ = (1:A) := by rewrite [-mul_one, inv_mul_cancel (ne.symm (@zero_ne_one A _))] theorem div_one : a / 1 = a := - by rewrite [↑divide, inv_one_is_one, mul_one] + by rewrite [↑divide, one_inv_eq, mul_one] theorem zero_div : 0 / a = 0 := !zero_mul @@ -92,7 +91,7 @@ section division_ring absurd C1 Ha theorem mul_ne_zero_comm (H : a * b ≠ 0) : b * a ≠ 0 := - have H2 : a ≠ 0 ∧ b ≠ 0, from mul_ne_zero_imp_ne_zero H, + have H2 : a ≠ 0 ∧ b ≠ 0, from ne_zero_and_ne_zero_of_mul_ne_zero H, mul_ne_zero' (and.right H2) (and.left H2) @@ -165,9 +164,7 @@ section division_ring theorem eq_of_invs_eq (Ha : a ≠ 0) (Hb : b ≠ 0) (H : 1 / a = 1 / b) : a = b := by rewrite [-(div_div Ha), H, (div_div Hb)] - -- oops, the analogous theorem in group is called inv_mul, but it *should* be called - -- mul_inv, in which case, we will have to rename this one - theorem mul_inv (Ha : a ≠ 0) (Hb : b ≠ 0) : (b * a)⁻¹ = a⁻¹ * b⁻¹ := + theorem mul_inv_eq (Ha : a ≠ 0) (Hb : b ≠ 0) : (b * a)⁻¹ = a⁻¹ * b⁻¹ := have H1 : b * a ≠ 0, from mul_ne_zero' Hb Ha, eq.symm (calc a⁻¹ * b⁻¹ = (1 / a) * b⁻¹ : inv_eq_one_div @@ -234,7 +231,7 @@ section field by rewrite [(one_div_mul_one_div Ha Hb), mul.comm b] theorem div_mul_right (Hb : b ≠ 0) (H : a * b ≠ 0) : a / (a * b) = 1 / b := - let Ha : a ≠ 0 := and.left (mul_ne_zero_imp_ne_zero H) in + let Ha : a ≠ 0 := and.left (ne_zero_and_ne_zero_of_mul_ne_zero H) in symm (calc 1 / b = 1 * (1 / b) : one_mul ... = (a * a⁻¹) * (1 / b) : mul_inv_cancel Ha @@ -259,7 +256,7 @@ section field by rewrite [add.comm, -(div_mul_left Ha H), -(div_mul_right Hb H), ↑divide, -right_distrib] theorem div_mul_div (Hb : b ≠ 0) (Hd : d ≠ 0) : (a / b) * (c / d) = (a * c) / (b * d) := - by rewrite [↑divide, 2 mul.assoc, (mul.comm b⁻¹), mul.assoc, (mul_inv Hd Hb)] + by rewrite [↑divide, 2 mul.assoc, (mul.comm b⁻¹), mul.assoc, (mul_inv_eq Hd Hb)] theorem mul_div_mul_left (Hb : b ≠ 0) (Hc : c ≠ 0) : (c * a) / (c * b) = a / b := have H [visible] : c * b ≠ 0, from mul_ne_zero' Hc Hb, @@ -400,7 +397,7 @@ section discrete_field (assume Ha : a ≠ 0, decidable.by_cases (assume Hb : b = 0, by rewrite [Hb, zero_mul, 2 inv_zero, mul_zero]) - (assume Hb : b ≠ 0, mul_inv Ha Hb)) + (assume Hb : b ≠ 0, mul_inv_eq Ha Hb)) -- the following are specifically for fields theorem one_div_mul_one_div''' : (1 / a) * (1 / b) = 1 / (a * b) := diff --git a/library/algebra/group.lean b/library/algebra/group.lean index f5dc9526c..9229ee9f3 100644 --- a/library/algebra/group.lean +++ b/library/algebra/group.lean @@ -1,8 +1,6 @@ /- Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: algebra.group Authors: Jeremy Avigad, Leonardo de Moura Various multiplicative and additive structures. Partially modeled on Isabelle's library. @@ -174,7 +172,7 @@ section group theorem inv_eq_of_mul_eq_one {a b : A} (H : a * b = 1) : a⁻¹ = b := by rewrite [-mul_one a⁻¹, -H, inv_mul_cancel_left] - theorem inv_one : 1⁻¹ = (1 : A) := inv_eq_of_mul_eq_one (one_mul 1) + theorem one_inv : 1⁻¹ = (1 : A) := inv_eq_of_mul_eq_one (one_mul 1) theorem inv_inv (a : A) : (a⁻¹)⁻¹ = a := inv_eq_of_mul_eq_one (mul.left_inv a) @@ -185,7 +183,7 @@ section group iff.intro (assume H, inv.inj H) (assume H, congr_arg _ H) theorem inv_eq_one_iff_eq_one (a b : A) : a⁻¹ = 1 ↔ a = 1 := - inv_one ▸ inv_eq_inv_iff_eq a 1 + one_inv ▸ inv_eq_inv_iff_eq a 1 theorem eq_inv_of_eq_inv {a b : A} (H : a = b⁻¹) : b = a⁻¹ := by rewrite [H, inv_inv] @@ -210,7 +208,7 @@ section group ... = a * 1 : mul.right_inv ... = a : mul_one - theorem inv_mul (a b : A) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := + theorem mul_inv (a b : A) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := inv_eq_of_mul_eq_one (calc a * b * (b⁻¹ * a⁻¹) = a * (b * (b⁻¹ * a⁻¹)) : mul.assoc diff --git a/library/algebra/group_power.lean b/library/algebra/group_power.lean index 3e670ddb0..353f44add 100644 --- a/library/algebra/group_power.lean +++ b/library/algebra/group_power.lean @@ -76,8 +76,8 @@ include s section nat open nat theorem inv_pow (a : A) : ∀n, (a⁻¹)^n = (a^n)⁻¹ -| 0 := by rewrite [*pow_zero, inv_one] -| (succ n) := by rewrite [pow_succ, pow_succ', inv_pow, inv_mul] +| 0 := by rewrite [*pow_zero, one_inv] +| (succ n) := by rewrite [pow_succ, pow_succ', inv_pow, mul_inv] theorem pow_sub (a : A) {m n : ℕ} (H : m ≥ n) : a^(m - n) = a^m * (a^n)⁻¹ := assert H1 : m - n + n = m, from nat.sub_add_cancel H, @@ -110,7 +110,7 @@ or.elim (nat.lt_or_ge m (nat.succ n)) ... = (pow a (nat.succ n) * (pow a m)⁻¹)⁻¹ : by rewrite [nat.succ_pred_of_pos H1, pow_sub a (nat.le_of_lt H)] ... = pow a m * (pow a (nat.succ n))⁻¹ : - by rewrite [inv_mul, inv_inv] + by rewrite [mul_inv, inv_inv] ... = ipow a (of_nat m) * ipow a (-[n +1]) : rfl) (assume H : (#nat m ≥ nat.succ n), calc @@ -126,7 +126,7 @@ theorem ipow_add (a : A) : ∀i j : int, ipow a (i + j) = ipow a i * ipow a j | -[ m+1] -[n+1] := calc ipow a (-[ m+1] + -[n+1]) = (a^(#nat nat.succ m + nat.succ n))⁻¹ : rfl - ... = (a^(nat.succ m))⁻¹ * (a^(nat.succ n))⁻¹ : by rewrite [pow_add, pow_comm, inv_mul] + ... = (a^(nat.succ m))⁻¹ * (a^(nat.succ n))⁻¹ : by rewrite [pow_add, pow_comm, mul_inv] ... = ipow a (-[ m+1]) * ipow a (-[n+1]) : rfl theorem ipow_comm (a : A) (i j : ℤ) : ipow a i * ipow a j = ipow a j * ipow a i := diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index 5988b972e..30d73d14d 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -229,7 +229,7 @@ section ... = 0 : mul_zero, symm (neg_eq_of_add_eq_zero H) - theorem mul_ne_zero_imp_ne_zero {a b : A} (H : a * b ≠ 0) : a ≠ 0 ∧ b ≠ 0 := + theorem ne_zero_and_ne_zero_of_mul_ne_zero {a b : A} (H : a * b ≠ 0) : a ≠ 0 ∧ b ≠ 0 := have Ha : a ≠ 0, from (assume Ha1 : a = 0, have H1 : a * b = 0, by rewrite [Ha1, zero_mul],