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

Add interchange.

Browse source
This commit is contained in:
favonia 2017-06-07 12:03:00 -06:00
parent 7ed3e47e09
commit 610aa351b8
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
move_to_lib.hlean
View file

@ -180,6 +180,13 @@ namespace group
definition isomorphism_ap {A : Type} (F : A → Group) {a b : A} (p : a = b) : F a ≃g F b := definition isomorphism_ap {A : Type} (F : A → Group) {a b : A} (p : a = b) : F a ≃g F b :=
isomorphism_of_eq (ap F p) isomorphism_of_eq (ap F p)
definition interchange (G : AbGroup) (a b c d : G) : (a * b) * (c * d) = (a * c) * (b * d) :=
calc (a * b) * (c * d) = a * (b * (c * d)) : by exact mul.assoc a b (c * d)
... = a * ((b * c) * d) : by exact ap (λ bcd, a * bcd) (mul.assoc b c d)⁻¹
... = a * ((c * b) * d) : by exact ap (λ bc, a * (bc * d)) (mul.comm b c)
... = a * (c * (b * d)) : by exact ap (λ bcd, a * bcd) (mul.assoc c b d)
... = (a * c) * (b * d) : by exact (mul.assoc a c (b * d))⁻¹
end group open group end group open group
namespace function namespace function