mathematics in lean

Stream: general

[Alexandre Rademaker]

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]

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]

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

[Alexandre Rademaker]

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]

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

[Alexandre Rademaker]

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]

You're allowed to also use the other lemmas mentioned up to that point (but not the ring tactic).

[Kevin Buzzard]

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

[Alexandre Rademaker]

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]

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.