First off, thanks to the team for putting this amazing course together!
Problem 1.3.16 asks to prove $p^2 + q^2 + r^2 = -4$ with $p, q, r$ being rational numbers. The problem is that, iirc, rational numbers don't include imaginary numbers, hence the square of such should be non-negative. Therefore their sum should also be non-negative.
More interestingly, I can actually write up the proof as this and Lean happily accepts it?
example {p q r : ℚ} (h1 : p + q + r = 0) (h2 : p * q + p * r + q * r = 2) :
p ^ 2 + q ^ 2 + r ^ 2 = -4 :=
calc p ^ 2 + q ^ 2 + r ^ 2 = p * p + q * q + r * r := by ring
_ = (p + q + r) ^ 2 - 2 * (p * q + p * r + q * r) := by ring
_ = 0 ^ 2 - 2 * 2 := by rw [h1, h2]
_ = -4 := by ring
First off, thanks to the team for putting this amazing course together!
Problem 1.3.16 asks to prove$p^2 + q^2 + r^2 = -4$ with $p, q, r$ being rational numbers. The problem is that, iirc, rational numbers don't include imaginary numbers, hence the square of such should be non-negative. Therefore their sum should also be non-negative.
More interestingly, I can actually write up the proof as this and Lean happily accepts it?