Def MulSemiringAction.toRingAut

Modification history

2025-02-25 16:16

Mathlib/Algebra/Ring/Action/End.lean

chore: separate the automorphism groups from their tautological action (#22141) …

Modified MulSemiringAction.toRingAut View on Github →

2022-12-29 11:25

Mathlib/Algebra/Ring/Aut.lean

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

Added MulSemiringAction.toRingAut View on Github →