pdiv — Mathlib

English

If f and g are multiplicative, then pdiv f g is multiplicative.

Русский

Если f и g мультипликативны, то pdiv f g мультипликативна.

LaTeX

$$$\operatorname{IsMultiplicative}(pdiv\ f\ g)$$$

Lean4

@[arith_mult]
theorem pdiv [CommGroupWithZero R] {f g : ArithmeticFunction R} (hf : IsMultiplicative f) (hg : IsMultiplicative g) :
    IsMultiplicative (pdiv f g) :=
  ⟨by simp [hf, hg], fun {m n} cop =>
    by
    simp only [pdiv_apply, map_mul_of_coprime hf cop, map_mul_of_coprime hg cop, div_eq_mul_inv, mul_inv]
    apply mul_mul_mul_comm⟩

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