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

Make A in isomorphism_ap implicit.

Browse source
This commit is contained in:
favonia 2017-06-06 12:34:13 -06:00
parent d014e50cd7
commit e2a12f7db7
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
move_to_lib.hlean
View file

@ -97,7 +97,7 @@ end eq open eq
namespace group 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)
end group end group