Inconsistency in "Mathematics in Lean"?

Stream: new members

[Julian Külshammer]

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]

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

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

Thanks

[Jeremy Avigad]

Thanks for catching that! We'll fix it.

[Jeremy Avigad]

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