Def AddQuantale.leftAddResiduation

Modification history

2026-09-18 15:04
Mathlib/Algebra/Order/Quantale.lean
chore: catch up on a lot of `to_additive` debt (#43814) …
Deleted AddQuantale.leftAddResiduationView on Github →
2025-01-11 04:09
Mathlib/Algebra/Order/Quantale.lean
add a variable_alias for Quantale and AddQuantale (#19282) …
Added AddQuantale.leftAddResiduationView on Github →