Theorem FractionalIdeal.mul_le_mul_left

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.mul_le_mul_leftView on Github →
2025-11-12 13:54
Mathlib/RingTheory/FractionalIdeal/Basic.lean
refactor(FractionalIdeal): use algebraic order theory API (#29538) …
Added FractionalIdeal.mul_le_mul_leftView on Github →
2025-09-11 10:26
Mathlib/RingTheory/FractionalIdeal/Basic.lean
chore(Submodule): instantiate `MulLeftMono` instead of ad hoc lemma (#29168)
Deleted FractionalIdeal.mul_le_mul_leftView on Github →
2023-05-23 18:30
Mathlib/RingTheory/FractionalIdeal.lean
feat: port RingTheory.FractionalIdeal (#4243)
Added FractionalIdeal.mul_le_mul_leftView on Github →