zeta_prod_zeta — Mathlib

English

The zeta function multiplies with itself to yield the zeta function on the product order: (zeta 𝕜).prod (zeta 𝕜) = zeta 𝕜.

Русский

Функция зета при умножении сама на себя даёт зету на произведение порядков: (zeta 𝕜).prod (zeta 𝕜) = zeta 𝕜.

LaTeX

$$$ (\zeta 𝕜).prod (\zeta 𝕜) = \zeta 𝕜 $$$

Lean4

@[simp]
theorem zeta_prod_zeta [DecidableLE α] [DecidableLE β] :
    (zeta 𝕜).prod (zeta 𝕜) = (zeta 𝕜 : IncidenceAlgebra 𝕜 (α × β)) := by ext x y hxy; simp [hxy, hxy.1, hxy.2]

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