intCoe_mul — Mathlib

English

For integer-valued arithmetic functions f,g and a ring R, the coerced product equals the product of coerced functions: (↑(f * g) : ArithmeticFunction R) = ↑f * g.

Русский

Для ℤ-значных функций f,g и кольца R, произведение после приведения равно произведению приведения: ↑(f * g) = ↑f * g.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem intCoe_mul [Ring R] {f g : ArithmeticFunction ℤ} : (↑(f * g) : ArithmeticFunction R) = ↑f * g :=
  by
  ext n
  simp

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