pdiv_zeta — Mathlib

English

For DivisionSemiring R, and any arithmetic function f, pdiv f zeta = f.

Русский

Для DivisionSemiring R и любой функции f: ArithmeticFunction R, pdiv f zeta = f.

LaTeX

$$$$ pdiv f \zeta = f $$$$

Lean4

/-- This result only holds for `DivisionSemiring`s instead of `GroupWithZero`s because zeta takes
values in ℕ, and hence the coercion requires an `AddMonoidWithOne`. TODO: Generalise zeta -/
@[simp]
theorem pdiv_zeta [DivisionSemiring R] (f : ArithmeticFunction R) : pdiv f zeta = f :=
  by
  ext n
  cases n <;> simp

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