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

feat(library/algebra/group): add theorem eq_inv_of_mul_eq_one

Browse source
This commit is contained in:
Haitao Zhang 2015-07-15 18:43:47 -07:00
parent 9ba350098f
commit f4cbd98692
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/algebra/group.lean
View file

@ -206,6 +206,9 @@ section group
theorem eq_inv_iff_eq_inv (a b : A) : a = b⁻¹ ↔ b = a⁻¹ := theorem eq_inv_iff_eq_inv (a b : A) : a = b⁻¹ ↔ b = a⁻¹ :=
iff.intro !eq_inv_of_eq_inv !eq_inv_of_eq_inv iff.intro !eq_inv_of_eq_inv !eq_inv_of_eq_inv
theorem eq_inv_of_mul_eq_one {a b : A} (H : a * b = 1) : a = b⁻¹ :=
begin rewrite [eq_inv_iff_eq_inv], apply eq.symm, exact inv_eq_of_mul_eq_one H end
theorem mul.right_inv (a : A) : a * a⁻¹ = 1 := theorem mul.right_inv (a : A) : a * a⁻¹ = 1 :=
calc calc
a * a⁻¹ = (a⁻¹)⁻¹ * a⁻¹ : inv_inv a * a⁻¹ = (a⁻¹)⁻¹ * a⁻¹ : inv_inv