Zulip Chat Archive

Stream: new members

Topic: Inconsistency in "Mathematics in Lean"?

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.

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.

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

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.

Kevin Buzzard (Jul 05 2020 at 08:04):


Jeremy Avigad (Jul 05 2020 at 12:30):

Thanks for catching that! We'll fix it.

Jeremy Avigad (Jul 05 2020 at 12:34):

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

Last updated: Dec 20 2023 at 11:08 UTC