Commit 2025-09-11 10:26 ceac2681

View on Github →

chore(Submodule): instantiate MulLeftMono instead of ad hoc lemma (#29168)

Estimated changes

Modified Mathlib/Algebra/Algebra/Operations.lean

deleted theorem Submodule.mul_le_mul

deleted theorem Submodule.mul_le_mul_left

deleted theorem Submodule.mul_le_mul_right

Modified Mathlib/Algebra/Polynomial/CoeffMem.lean

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

Modified Mathlib/RingTheory/DedekindDomain/PID.lean

Modified Mathlib/RingTheory/Finiteness/Subalgebra.lean

Modified Mathlib/RingTheory/FractionalIdeal/Basic.lean

deleted theorem FractionalIdeal.add_le_add_left

deleted theorem FractionalIdeal.mul_le_mul_left

Modified Mathlib/RingTheory/Spectrum/Prime/Basic.lean