Theorem FractionalIdeal.add_le_add_left

Modification history

2025-09-11 10:26
Mathlib/RingTheory/FractionalIdeal/Basic.lean
chore(Submodule): instantiate `MulLeftMono` instead of ad hoc lemma (#29168)
Deleted FractionalIdeal.add_le_add_leftView on Github →
2023-05-23 18:30
Mathlib/RingTheory/FractionalIdeal.lean
feat: port RingTheory.FractionalIdeal (#4243)
Added FractionalIdeal.add_le_add_leftView on Github →