Def Ring.ordFrac

Modification history

2025-07-04 09:20

Mathlib/RingTheory/OrderOfVanishing.lean

feat(WithZero): `exp : ℤ → ℤᵐ⁰`, `log : ℤᵐ⁰ → ℤ` (#24977) …

Modified Ring.ordFrac View on Github →

2025-06-16 08:23

Mathlib/RingTheory/OrderOfVanishing.lean

feat(RingTheory): Order of vanishing in a ring (#25255) …

Added Ring.ordFrac View on Github →