Def MulSemiringAction.toRingAut

Modification history

2022-12-29 11:25
Mathlib/Algebra/Ring/Aut.lean
feat: port Algebra.Ring.Aut (#1228) …
Added MulSemiringAction.toRingAutView on Github →