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

refactor(library): cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-22 14:10:02 -08:00
parent 6fc0e41439
commit 564e8f947d
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/algebra/group.lean
View file

@ -297,7 +297,7 @@ section group
lemma is_conj.symm (a b : A) : a ~ b → b ~ a := lemma is_conj.symm (a b : A) : a ~ b → b ~ a :=
assume Pab, obtain x (Pconj : x ∘c b = a), from Pab, assume Pab, obtain x (Pconj : x ∘c b = a), from Pab,
assert Pxinv : x⁻¹ ∘c x ∘c b = x⁻¹ ∘c a, from (congr_arg2 conj_by (eq.refl x⁻¹) Pconj), assert Pxinv : x⁻¹ ∘c x ∘c b = x⁻¹ ∘c a, begin congruence, assumption end,
exists.intro x⁻¹ (eq.symm (conj_inv_cancel x b ▸ Pxinv)) exists.intro x⁻¹ (eq.symm (conj_inv_cancel x b ▸ Pxinv))
lemma is_conj.trans (a b c : A) : a ~ b → b ~ c → a ~ c := lemma is_conj.trans (a b c : A) : a ~ b → b ~ c → a ~ c :=

2
library/init/logic.lean
View file

@ -347,7 +347,7 @@ iff_true_intro not_false
theorem not_congr [congr] (H : a ↔ b) : ¬a ↔ ¬b := theorem not_congr [congr] (H : a ↔ b) : ¬a ↔ ¬b :=
iff.intro (λ H₁ H₂, H₁ (iff.mpr H H₂)) (λ H₁ H₂, H₁ (iff.mp H H₂)) iff.intro (λ H₁ H₂, H₁ (iff.mpr H H₂)) (λ H₁ H₂, H₁ (iff.mp H H₂))
theorem ne_self_iff_false {A : Type} (a : A) : (a ≠ a) ↔ false := theorem ne_self_iff_false [simp] {A : Type} (a : A) : (not (a = a)) ↔ false :=
iff.intro false_of_ne false.elim iff.intro false_of_ne false.elim
theorem eq_self_iff_true [simp] {A : Type} (a : A) : (a = a) ↔ true := theorem eq_self_iff_true [simp] {A : Type} (a : A) : (a = a) ↔ true :=