Def AddAut.mulLeft

Modification history

2026-05-27 15:09

Mathlib/Algebra/Ring/AddAut.lean

refactor(GroupTheory/*): additivize `AddAut` (#39884) …

Modified AddAut.mulLeft View on Github →

2023-01-01 20:11

Mathlib/Algebra/Ring/AddAut.lean

feat: port Algebra.Ring.AddAut (#1284)

Added AddAut.mulLeft View on Github →