Section 2.2: Definition of substraction in a general ring

[yannickseurin]

Section 2.2: Definition of substraction in a general ring

[avigad]

Thanks for the input! In Lean's axiomatization of Ring (and in even more basic structures), the minus symbol and negation symbol are declared independently and the axioms imply a - b = a +-b. That gives users more flexibility in defining particular instances. For example, one can define subtraction and negation on the reals independently (e.g. in terms of Cauchy sequences) and then prove that they agree.

If the axioms fixed the definition of subtraction, we could have trouble whenever someone declared an instance that already has a subtraction defined. On the other hand, including subtraction in the structure and axiomatizing its behavior means that we can use the same generic theorems no matter how subtraction is defined in particular instances.

This is a common theme in Mathlib; see the discussion of diamond problems in Section 7.1. We plan to revise MIL soon and will clarify this.

[yannickseurin]

Thanks a lot for the answer! I'm still a bit new to Lean to understand it perfectly but I kind of see the idea!