ppow — Mathlib

English

For any multiplicative f, f.ppow k is multiplicative for any k.

Русский

Для любого мультипликативного f и любого k функция f.ppow k является мультипликативной.

LaTeX

$$$ IsMultiplicative (f.ppow k) $$$

Lean4

@[arith_mult]
theorem ppow [CommSemiring R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {k : ℕ} :
    IsMultiplicative (f.ppow k) := by
  induction k with
  | zero => exact isMultiplicative_zeta.natCast
  | succ k hi => rw [ppow_succ']; apply hf.pmul hi

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