Theorem FractionalIdeal.coeIdeal_le_self_mul_inv

Modification history

2026-11-10 17:26
Mathlib/RingTheory/FractionalIdeal/Inverse.lean
chore: correct naming of coercion lemmas about coeIdeal (#45832) …
Added FractionalIdeal.coeIdeal_le_self_mul_invView on Github →