intCast — Mathlib

English

If f is multiplicative with values in ℤ and R is a ring, then the cast of f to ArithmeticFunction R is multiplicative.

Русский

Если f мультипликативна и принимает значения в ℤ, то её отображение в ArithmeticFunction R также мультипликативна.

LaTeX

$$$\operatorname{IsMultiplicative}(f) \Rightarrow \operatorname{IsMultiplicative}(f: \text{ArithmeticFunction } R)$$$

Lean4

@[arith_mult]
theorem intCast {f : ArithmeticFunction ℤ} [Ring R] (h : f.IsMultiplicative) :
    IsMultiplicative (f : ArithmeticFunction R) :=
  ⟨by simp [h], fun {m n} cop => by simp [h.2 cop]⟩

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