Commit 2026-08-06 10:50 5edf93c0

View on Github →

chore(RingTheory): fix left/right convention on Ideal.mul_le_{left,right} (#42112) Swap Ideal.mul_le_left and Ideal.mul_le_right so that they follow the left/right naming convention.

Estimated changes

Modified Mathlib/RingTheory/AdicCompletion/Algebra.lean

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean

Modified Mathlib/RingTheory/DividedPowers/Basic.lean

Modified Mathlib/RingTheory/DividedPowers/SubDPIdeal.lean

Modified Mathlib/RingTheory/Extension/Basic.lean

Modified Mathlib/RingTheory/Extension/Cotangent/Basis.lean

Modified Mathlib/RingTheory/Finiteness/Ideal.lean

Modified Mathlib/RingTheory/Finiteness/NilpotentKer.lean

Modified Mathlib/RingTheory/Ideal/IsPrimary.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

modified theorem Ideal.mul_le_left

modified theorem Ideal.mul_le_right

Modified Mathlib/RingTheory/Ideal/Pure.lean

Modified Mathlib/RingTheory/Ideal/Quotient/Operations.lean

Modified Mathlib/RingTheory/Ideal/Quotient/PowTransition.lean

Modified Mathlib/RingTheory/Kaehler/JacobiZariski.lean

Modified Mathlib/RingTheory/PicardGroup.lean

Modified Mathlib/RingTheory/Polynomial/ContentIdeal.lean

Modified Mathlib/RingTheory/PrincipalIdealDomainOfPrime.lean

Modified Mathlib/RingTheory/Smooth/Quotient.lean

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