mul_to_nat — Mathlib

English

For all m,n, the Nat cast of m*n equals the Nat cast of m times the Nat cast of n: ((m * n : Num) : ℕ) = m * n.

Русский

Для всех m,n: преобразование в ℕ после умножения в Num эквивалентно умножению соответствующих преобразований: ((m * n : Num) : ℕ) = m * n.

LaTeX

$$$\\forall m,n,\\ ((m * n : Num) : \\mathbb{N}) = m * n$$$

Lean4

@[norm_cast]
theorem mul_to_nat : ∀ m n, ((m * n : Num) : ℕ) = m * n
  | 0, 0 => rfl
  | 0, pos _q => (zero_mul _).symm
  | pos _p, 0 => rfl
  | pos _p, pos _q => PosNum.mul_to_nat _ _

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