Def Ring.ordMonoidWithZeroHom

Modification history

2025-07-04 09:20
Mathlib/RingTheory/OrderOfVanishing.lean
feat(WithZero): `exp : ℤ → ℤᵐ⁰`, `log : ℤᵐ⁰ → ℤ` (#24977) …
Modified Ring.ordMonoidWithZeroHomView on Github →
2025-06-16 08:23
Mathlib/RingTheory/OrderOfVanishing.lean
feat(RingTheory): Order of vanishing in a ring (#25255) …
Added Ring.ordMonoidWithZeroHomView on Github →