zeta_mul_zeta — Mathlib

English

(zeta 𝕜 * zeta 𝕜)(a,b) equals card(Icc a b) cast to 𝕜; the product of zeta with itself counts the interval.

Русский

(zeta 𝕜 * zeta 𝕜)(a,b) равно кардиналу(Icc a b) приведённому к 𝕜; произведение зета на себя считает интервал.

LaTeX

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

Lean4

theorem zeta_mul_zeta [NonAssocSemiring 𝕜] [Preorder α] [LocallyFiniteOrder α] [DecidableLE α] (a b : α) :
    (zeta 𝕜 * zeta 𝕜 : IncidenceAlgebra 𝕜 α) a b = (Icc a b).card :=
  by
  rw [mul_apply, card_eq_sum_ones, Nat.cast_sum, Nat.cast_one]
  refine sum_congr rfl fun x hx ↦ ?_
  rw [mem_Icc] at hx
  rw [zeta_of_le hx.1, zeta_of_le hx.2, one_mul]

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