mu_mul_zeta — Mathlib

English

The convolution of zeta with itself again yields the interval cardinality formula: (zeta 𝕜 * zeta 𝕜)(a,b) = card(Icc a b) in 𝕜.

Русский

Свёртка зеты с самой собой снова возвращает формулу кардинальности интервала: (zeta 𝕜 * zeta 𝕜)(a,b) = card(Icc a b) в 𝕜.

LaTeX

$$$ (zeta 𝕜 * zeta 𝕜)(a,b) = (\# Icc a b) : 𝕜 $$$

Lean4

theorem mu_mul_zeta : (mu 𝕜 * zeta 𝕜 : IncidenceAlgebra 𝕜 α) = 1 :=
  by
  ext a b
  calc
    _ = ∑ x ∈ Icc a b, mu 𝕜 a x := by rw [mul_apply]; congr! with x hx; simp [(mem_Icc.1 hx).2]
    _ = (1 : IncidenceAlgebra 𝕜 α) a b := sum_Icc_mu_right ..

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