## Stream: general

### 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 ring` tactic).

#### 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