Theorem RingHom.coe_one

Modification history

2024-06-05 08:10

Mathlib/Algebra/Ring/Hom/Defs.lean

refactor: Redefine `pow` in terms of `iterate` (#1388) …

Modified RingHom.coe_one View on Github →

2022-12-13 11:06

Mathlib/Algebra/Hom/Ring.lean

feat: Port `Algebra.Hom.Ring` (#958) …

Added RingHom.coe_one View on Github →