pmul — Mathlib

English

If f and g are multiplicative, then their pointwise product f.pmul g is multiplicative.

Русский

Если f и g мультипликативны, то их точечное произведение f.pmul g также мультипликативно.

LaTeX

$$$\operatorname{IsMultiplicative}(f) \land \operatorname{IsMultiplicative}(g) \Rightarrow \operatorname{IsMultiplicative}(f\,\text{pmul}\, g)$$$

Lean4

@[arith_mult]
theorem pmul [CommSemiring R] {f g : ArithmeticFunction R} (hf : f.IsMultiplicative) (hg : g.IsMultiplicative) :
    IsMultiplicative (f.pmul g) :=
  ⟨by simp [hf, hg], fun {m n} cop =>
    by
    simp only [pmul_apply, hf.map_mul_of_coprime cop, hg.map_mul_of_coprime cop]
    ring⟩

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