Theorems · Theorem · number theory

ArithmeticFunction.sum_divisorsAntidiagonal_eq_sum_divisors

∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : MulAction R M]
  {f : ArithmeticFunction M} {x : ℕ},
  (∑ x ∈ x.divisorsAntidiagonal, if x.1 = 0 then 0 • f x.2 else f x.2) = ∑ i ∈ x.divisors, f i

@[simp]-normal form of coe_zeta_smul_apply.

Defined in

Mathlib.NumberTheory.ArithmeticFunction.Zeta

Cited by

0 results in Mathlib

Foundations

Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidMulAction