English
Sign is multiplicative: sign(xy) = sign(x) · sign(y) for EReal.
Русский
Знак умножения сохраняется: sign(xy) = sign(x) · sign(y) в EReal.
LaTeX
$$$ \operatorname{sign}(xy) = \operatorname{sign}(x) \cdot \operatorname{sign}(y) $$$
Lean4
@[simp]
theorem sign_mul (x y : EReal) : sign (x * y) = sign x * sign y := by
induction x, y using induction₂_symm_neg with
| top_zero => simp only [mul_zero, sign_zero]
| top_top => rfl
| symm h => rwa [mul_comm, EReal.mul_comm]
| coe_coe => simp only [← coe_mul, sign_coe, _root_.sign_mul]
| top_pos _ h => rw [top_mul_coe_of_pos h, sign_top, one_mul, sign_pos (EReal.coe_pos.2 h)]
| neg_left h => rw [neg_mul, sign_neg, sign_neg, h, neg_mul]
