Commit 2022-12-29 11:25 1af1afa6

View on Github →

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

depends on: #1225

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Ring/Aut.lean

added def MulSemiringAction.toRingAut

added def RingAut.toAddAut

added def RingAut.toMulAut

added def RingAut.toPerm

added def RingAut