subtraction in ring

Stream: new members

[Alex Zhang]

It seems rfl does not solve example (a b : R) : a - b = a + -b := . I am wondering how subtraction is defined in ring. I tried to "peek" the definition of -, but I only found class has_sub (α : Type u) := (sub : α → α → α).

[Ruben Van de Velde]

Depends on the ring

[Johan Commelin]

@Alex Zhang A ring (in mathlib) comes with addition, negation, and subtraction, plus an axiom sub_eq_add_neg that relates them.

[Alex Zhang]

OK. I thought a -b is just a + (-b) by definition.

[Johan Commelin]

It used to be, but it changed about half a year ago.

[Kevin Buzzard]

It doesn't matter whether it's a definition or not -- it's still a theorem.

[Kevin Buzzard]

Mathematicians should use an object via its interface, as opposed to peeking inside and seeing its definition. You don't want to know the definition of metric space or group in Lean -- neither of them are at all what you think they are. All that matters is that given enough data to make what you think a metric space is, there's a function which will construct a metric space from that data in Lean.