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).