cast_mul — Mathlib

English

For any Num m,n and any α with a non-associative semiring, the cast respects multiplication: (m * n : Num) cast equals (m cast) times (n cast).

Русский

Для любых Num m,n и α с неассоциативной полугруппой с умножением, приведение сохраняет умножение: ((m * n) : α) = (m : α) · (n : α).

LaTeX

$$$((m \cdot n : Num) : \alpha) = (m : \alpha) \cdot (n : \alpha)$$$

Lean4

@[simp, norm_cast]
theorem cast_mul [NonAssocSemiring α] : ∀ m n, ((m * n : Num) : α) = m * n
  | 0, 0 => (zero_mul _).symm
  | 0, pos _q => (zero_mul _).symm
  | pos _p, 0 => (mul_zero _).symm
  | pos _p, pos _q => PosNum.cast_mul _ _

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