Theorem FractionalIdeal.le_div_iff_of_ne_zero

Modification history

2025-11-12 13:54
Mathlib/RingTheory/FractionalIdeal/Operations.lean
refactor(FractionalIdeal): use algebraic order theory API (#29538) …
Added FractionalIdeal.le_div_iff_of_ne_zeroView on Github →