michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix({hott,library}/algebra/*): fix names

Browse source
This commit is contained in:
Jeremy Avigad 2015-05-23 14:05:06 +10:00
parent 4bc93b59e3
commit d33c91d7b9
7 changed files with 26 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
hott/algebra/field.hlean
View file

@ -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) :=

6
hott/algebra/group.hlean
View file

@ -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

2
hott/algebra/ring.hlean
View file

@ -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],

17
library/algebra/field.lean
View file

@ -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) :=

8
library/algebra/group.lean
View file

@ -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

8
library/algebra/group_power.lean
View file

@ -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 :=

2
library/algebra/ring.lean
View file

@ -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],