Commit 2025-06-11 15:07 efe911a4

View on Github →

chore(RingTheory/DedekindDomain): missing instances (#25613)

Estimated changes

Modified Mathlib/Algebra/Algebra/Operations.lean

Modified Mathlib/Algebra/Order/GroupWithZero/Unbundled/OrderIso.lean

added theorem inf_mul₀

added theorem mul_inf₀

added theorem mul_sup₀

added theorem sup_mul₀

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

added theorem FractionalIdeal.inf_mul

added theorem FractionalIdeal.mul_inf

added theorem Ideal.iInf_mul

added theorem Ideal.inf_mul

added theorem Ideal.mul_iInf

added theorem Ideal.mul_inf

Modified Mathlib/RingTheory/FractionalIdeal/Basic.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

added theorem Ideal.iSup_mul

added theorem Ideal.mul_iSup