Skip to content

Commit

Permalink
do not rename instance
Browse files Browse the repository at this point in the history
  • Loading branch information
AntoineChambert-Loir committed Jan 5, 2025
1 parent 7d04a99 commit f329b56
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Group/Aut.lean
Original file line number Diff line number Diff line change
Expand Up @@ -160,7 +160,7 @@ variable (A) [Add A]
/-- The group operation on additive automorphisms is defined by `g h => AddEquiv.trans h g`.
This means that multiplication agrees with composition, `(g*h)(x) = g (h x)`.
-/
instance instGroup : Group (AddAut A) where
instance : Group (AddAut A) where
mul g h := AddEquiv.trans h g
one := AddEquiv.refl _
inv := AddEquiv.symm
Expand Down

0 comments on commit f329b56

Please sign in to comment.