natCast — Mathlib

English

If f is multiplicative on ℕ and R is a semiring, then the cast of f to ArithmeticFunction R is multiplicative.

Русский

Если f мультипликативна на ℕ и R — полуребро полного кольца, то отображение f в ArithmeticFunction R сохраняет мультипликативность.

LaTeX

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

Lean4

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

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