Theorem OrderMonoidWithZeroHom.toMonoidWithZeroHom_eq_ofClass

Modification history

2026-09-16 13:44

Mathlib/Algebra/Order/Hom/MonoidWithZero.lean

fix(Algebra/MonoidWithZeroHom): normalize to `.toMonoidWithZeroHom` (#43728) …

Deleted OrderMonoidWithZeroHom.toMonoidWithZeroHom_eq_ofClass View on Github →

2026-06-06 05:44

Mathlib/Algebra/Order/Hom/MonoidWithZero.lean

fix(RingTheory/Valuation): change `ValueGroup` from taking HomClass to Hom (#36911) …

Added OrderMonoidWithZeroHom.toMonoidWithZeroHom_eq_ofClass View on Github →