Theorem FractionalIdeal.le_self_mul_self

Modification history

2026-03-25 05:05
Mathlib/RingTheory/FractionalIdeal/Basic.lean
chore: remove declarations deprecated between 2021-03-24 and 2025-09-24 (#37118) …
Deleted FractionalIdeal.le_self_mul_selfView on Github →
2025-11-12 13:54
Mathlib/RingTheory/FractionalIdeal/Basic.lean
refactor(FractionalIdeal): use algebraic order theory API (#29538) …
Modified FractionalIdeal.le_self_mul_selfView on Github →
2023-05-23 18:30
Mathlib/RingTheory/FractionalIdeal.lean
feat: port RingTheory.FractionalIdeal (#4243)
Added FractionalIdeal.le_self_mul_selfView on Github →