diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 81cabe3..1b52a94 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -97,7 +97,7 @@ end eq open eq 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) end group