Zulip Chat Archive

Stream: new members

Topic: subtraction in ring


Alex Zhang (May 28 2021 at 09:43):

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 (May 28 2021 at 09:44):

Depends on the ring

Johan Commelin (May 28 2021 at 09:45):

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

Alex Zhang (May 28 2021 at 09:46):

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

Johan Commelin (May 28 2021 at 09:47):

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

Kevin Buzzard (May 28 2021 at 12:52):

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

Kevin Buzzard (May 28 2021 at 12:53):

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.


Last updated: Dec 20 2023 at 11:08 UTC