Commit 2025-01-11 04:09 8df90d17

View on Github →

add a variable_alias for Quantale and AddQuantale (#19282) similar to #19212, but for Quantales, taken from the variable_alias docs. Zulip: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/why.20.5Bvariable_alias.5D.20attribute.20is.20not.20used.20in.20Mathlib.3F

Estimated changes

Modified Mathlib/Algebra/Order/Quantale.lean

added def AddQuantale.leftAddResiduation

added def AddQuantale.rightAddResiduation

added structure AddQuantale

deleted def IsAddQuantale.leftAddResiduation

deleted def IsAddQuantale.rightAddResiduation

deleted theorem IsQuantale.bot_mul

deleted theorem IsQuantale.iSup_mul_distrib

deleted def IsQuantale.leftMulResiduation

deleted theorem IsQuantale.leftMulResiduation_le_iff_mul_le

deleted theorem IsQuantale.mul_bot

deleted theorem IsQuantale.mul_iSup_distrib

deleted theorem IsQuantale.mul_sup_distrib

deleted def IsQuantale.rightMulResiduation

deleted theorem IsQuantale.rightMulResiduation_le_iff_mul_le

deleted theorem IsQuantale.sup_mul_distrib

added theorem Quantale.bot_mul

added theorem Quantale.iSup_mul_distrib

added def Quantale.leftMulResiduation

added theorem Quantale.leftMulResiduation_le_iff_mul_le

added theorem Quantale.mul_bot

added theorem Quantale.mul_iSup_distrib

added theorem Quantale.mul_sup_distrib

added def Quantale.rightMulResiduation

added theorem Quantale.rightMulResiduation_le_iff_mul_le

added theorem Quantale.sup_mul_distrib

added structure Quantale