natCoe_mul — Mathlib

English

For natural-valued arithmetic functions f,g, the coerced product equals the product of coerced functions: ↑(f * g) = f * g in ArithmeticFunction R.

Русский

Для ℕ-значных функций произведение согласуется с приводимым: ↑(f * g) = f * g в ArithmeticFunction R.

LaTeX

$$$\\uparrow\\,(f * g) = f * g$ in ArithmeticFunction(R)$$

Lean4

@[simp, norm_cast]
theorem natCoe_mul [Semiring R] {f g : ArithmeticFunction ℕ} : (↑(f * g) : ArithmeticFunction R) = f * g :=
  by
  ext n
  simp

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