mathematics_in_lean_source
mathematics_in_lean_source copied to clipboard
`|a * b| ≤ (a ^ 2 + b ^ 2) / 2` exercise uses `constructor` before it is introduced
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.
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.