English
The absolute value is multiplicative on EReal: the absolute value of a product equals the product of absolute values.
Русский
Модульность сохраняется под умножением: |xy| = |x| |y| на EReal.
LaTeX
$$$ |xy| = |x| \cdot |y| \quad \text{in } \mathrm{EReal} $$$
Lean4
@[simp]
theorem abs_mul (x y : EReal) : (x * y).abs = x.abs * y.abs := by
induction x, y using induction₂_symm_neg with
| top_zero => simp only [mul_zero, abs_zero]
| top_top => rfl
| symm h => rwa [mul_comm, EReal.mul_comm]
| coe_coe => simp only [← coe_mul, abs_def, _root_.abs_mul, ENNReal.ofReal_mul (abs_nonneg _)]
| top_pos _ h =>
rw [top_mul_coe_of_pos h, abs_top, ENNReal.top_mul]
rw [Ne, abs_eq_zero_iff, coe_eq_zero]
exact h.ne'
| neg_left h => rwa [neg_mul, EReal.abs_neg, EReal.abs_neg]
