natCast_mul — Mathlib

English

The natural-number embedding preserves multiplication: (m * n : EReal) = (m : EReal) * (n : EReal).

Русский

Встраивание натуральных чисел сохраняет умножение: (m * n : EReal) = (m : EReal) * (n : EReal).

LaTeX

$$$ (m * n : \mathrm{EReal}) = (m : \mathrm{EReal}) \cdot (n : \mathrm{EReal}) $$$

Lean4

@[simp, norm_cast]
theorem natCast_mul (m n : ℕ) : (m * n : ℕ) = (m : EReal) * (n : EReal) := by
  rw [← coe_coe_eq_natCast, ← coe_coe_eq_natCast, ← coe_coe_eq_natCast, Nat.cast_mul, EReal.coe_mul]

Похожие утверждения