Topic: mathematics in lean
Alexandre Rademaker (Sep 05 2020 at 15:36):
In chapter 2, one proposed exercise says "The following exercise is a little more challenging. You can use the theorems listed underneath." The problem is to prove
example (a b : ℝ) : (a + b) * (a - b) = a^2 - b^2. I wonder if I should read as `ONLY using the theorems listed underneath or I have to consider other theorems too, such as add_assoc...
Alexandre Rademaker (Sep 05 2020 at 15:42):
BTW, is there any option that I can set up in Lean to ALWAYS show the parenthesis? I would like to be able to see
(a + b) + c when I write
a + b + c.
Kevin Buzzard (Sep 05 2020 at 16:02):
I remember wishing for this once but I don't think you can have it :-(
Alexandre Rademaker (Sep 05 2020 at 16:03):
The best I could get was the prefix notation (sub a b) for
a - b... but it didn't turn the term more legible in the end!
Kenny Lau (Sep 05 2020 at 16:05):
just remember that the default is
(a + b) + c
Alexandre Rademaker (Sep 05 2020 at 16:07):
Yes, I know... but it is hard to keep that in mind. @Kevin Buzzard created a quite challenging exercise OR I may have misinterpreted the restrictions to solve it.
Patrick Massot (Sep 05 2020 at 16:20):
You're allowed to also use the other lemmas mentioned up to that point (but not the
Kevin Buzzard (Sep 05 2020 at 19:32):
I do not remember setting that exercise and suspect it was Patrick or Jeremy
Alexandre Rademaker (Sep 06 2020 at 19:28):
Solved yesterday with the clarification from @Patrick Massot ! In the end, it was my mistake in the restricted interpretation. It is quite obvious that add_comm is surely needed.
Alexandre Rademaker (Sep 06 2020 at 19:29):
Solved yesterday with the clarification from Patrick! In the end, it was my mistake in the restricted interpretation. It is quite obvious that mil_comm is surely needed.
Last updated: May 12 2021 at 23:13 UTC