Section 2.2: Definition of substraction in a general ring

[yannickseurin]

I'm currently going through MIL and everything reads really well, but this passage in Section 2.2 made me pause and wonder:

In Lean, subtraction in a ring is provably equal to addition of the additive inverse.

example (a b : R) : a - b = a + -b :=
sub_eq_add_neg a b

On the real numbers, it is defined that way:

I don't see how substraction might be defined differently from "addition of the additive inverse" in a general ring. Maybe this is too advanced stuff to explain at this point, but it might be nice to comment even informally on this (I searched sub_eq_add_neg in mathlib4 doc but this isn't very informative).

[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!