toNat_mul — Mathlib

English

toNat(a*b) = toNat(a) * toNat(b).

Русский

toNat(a*b) = toNat(a) * toNat(b).

LaTeX

$$$\\\\forall a,b \\\\in \\\\mathbb{N}_{\\\\infty}, \\\\operatorname{toNat}(a b) = \\\\operatorname{toNat}(a) \\\\cdot \\\\operatorname{toNat}(b)$$$

Lean4

@[simp]
theorem toNat_mul (a b : ℕ∞) : (a * b).toNat = a.toNat * b.toNat :=
  by
  cases a <;> cases b
  · simp
  · rename_i b; cases b <;> simp
  · rename_i a; cases a <;> simp
  · simp only [toNat_coe]; rw [← coe_mul, toNat_coe]

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