Zulip Chat Archive

Stream: general

Topic: mathematics in lean


view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 05 2020 at 16:02):

I remember wishing for this once but I don't think you can have it :-(

view this post on Zulip 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!

view this post on Zulip Kenny Lau (Sep 05 2020 at 16:05):

just remember that the default is (a + b) + c

view this post on Zulip 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.

view this post on Zulip 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 ring tactic).

view this post on Zulip Kevin Buzzard (Sep 05 2020 at 19:32):

I do not remember setting that exercise and suspect it was Patrick or Jeremy

view this post on Zulip 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.

view this post on Zulip 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