mathematics_in_lean_source icon indicating copy to clipboard operation
mathematics_in_lean_source copied to clipboard

`|a * b| ≤ (a ^ 2 + b ^ 2) / 2` exercise uses `constructor` before it is introduced

Open kmill opened this issue 1 year ago • 1 comments

The challenge exercise at the end of section 2.3 proving |a * b| ≤ (a ^ 2 + b ^ 2) / 2 uses the constructor tactic, but this tactic is not introduced until section 3.4.

kmill avatar Oct 20 '23 04:10 kmill

For now, I added a stopgap fix which tells the reader that they will need to use constructor to split the conjunction and gives a reference to 3.4. We should revisit whether to keep this fix, change the exercise, or just delete it.

avigad avatar Oct 22 '23 18:10 avigad