Theorem MonoidHom.ext_mnat

Modification history

2025-01-25 06:17

Mathlib/Algebra/Group/Nat/Hom.lean

chore(Data/Nat/Cast): don't import `MonoidWithZero` for results about `MonoidHom` (#20745) …

Modified MonoidHom.ext_mnat View on Github →

2024-01-09 09:25

Mathlib/Algebra/GroupPower/Lemmas.lean

chore: Move `Int` and `Nat` cast lemmas (#9503) …

Modified MonoidHom.ext_mnat View on Github →

2022-12-19 11:23

Mathlib/Algebra/GroupPower/Lemmas.lean

feat port Algebra.GroupPower.Lemmas (#1055) …

Added MonoidHom.ext_mnat View on Github →