Stream: new members
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):
a + b + -b = a can be proved by
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: May 11 2021 at 13:22 UTC