Zulip Chat Archive

Stream: new members

Topic: Inconsistency in "Mathematics in Lean"?


view this post on Zulip Julian Külshammer (Jul 05 2020 at 07:07):

Hi. I'm currently working through the tutorial "Mathematics in Lean". In Section 2.2 "Proving Identities in Algebraic Structures" one is asked to "reprove" theorems from the library. One of the first is neg_add_cancel_right, which is a + b + -b=a. However, if I do #check neg_add_cancel_right later on to check what is in the library it tells me that this is a + -b + b = a.

view this post on Zulip Bryan Gin-ge Chen (Jul 05 2020 at 07:11):

It's likely that this was renamed since that part of the text was written.

view this post on Zulip Bryan Gin-ge Chen (Jul 05 2020 at 07:19):

Hmm, actually, I checked and it's probably just a typo / difference in applying naming conventions. @Jeremy Avigad

view this post on Zulip Bryan Gin-ge Chen (Jul 05 2020 at 07:21):

According to library_search, a + b + -b = a can be proved by add_neg_eq_of_eq_add rfl.

view this post on Zulip Kevin Buzzard (Jul 05 2020 at 08:04):

Thanks

view this post on Zulip Jeremy Avigad (Jul 05 2020 at 12:30):

Thanks for catching that! We'll fix it.

view this post on Zulip Jeremy Avigad (Jul 05 2020 at 12:34):

The correct name is add_neg_cancel_right (which is what it should be).


Last updated: May 11 2021 at 13:22 UTC