English
In the extended real line EReal, negation distributes over multiplication on the left: (-x) · y = -(x · y) for all x,y ∈ EReal.
Русский
В расширенном множестве вещественных чисел EReal отрицание распространяется на произведение слева: (-x)·y = -(x·y) для всех x,y ∈ EReal.
LaTeX
$$$ -x \\cdot y = -(x \\cdot y) $$$
Lean4
protected theorem neg_mul (x y : EReal) : -x * y = -(x * y) := by
induction x, y using induction₂_neg_left with
| top_zero
| zero_top
| zero_bot => simp only [zero_mul, mul_zero, neg_zero]
| top_top
| top_bot => rfl
| neg_left h => rw [h, neg_neg, neg_neg]
| coe_coe => norm_cast; exact neg_mul _ _
| top_pos _ h => rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
| pos_top _ h => rw [coe_mul_top_of_pos h, neg_top, ← coe_neg, coe_mul_top_of_neg (neg_neg_of_pos h)]
| top_neg _ h => rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
| pos_bot _ h => rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg, coe_mul_bot_of_neg (neg_neg_of_pos h)]
