Theorem FractionalIdeal.coe_inv_of_ne_zero

Modification history

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