Def RingAut.toAddAut

Modification history

2024-06-04 05:31

Mathlib/Algebra/Ring/Aut.lean

chore: remove some `refine'` replacing `refine_struct` (#13490) …

Modified RingAut.toAddAut View on Github →

2023-06-28 10:21

Mathlib/Algebra/Ring/Aut.lean

chore: cleanup porting notes about refine_struct (#5542) …

Modified RingAut.toAddAut View on Github →

2022-12-29 11:25

Mathlib/Algebra/Ring/Aut.lean

feat: port Algebra.Ring.Aut (#1228) …

Added RingAut.toAddAut View on Github →