factors_prod_eq_basis — Mathlib

English

If s is finite, the product of the elements of the list factors C s x equals the basis element spanFinBasis C s x.

Русский

Пусть s конечно. Тогда произведение элементов списка факторов C s x равно базисному элементу spanFinBasis C s x.

LaTeX

$$$ (factors\; C\; s\; x).prod = spanFinBasis\; C\; s\; x $$$

Lean4

/-- If `s` is finite, the product of the elements of the list `factors C s x`
is the delta function at `x`. -/
theorem factors_prod_eq_basis (x : π C (· ∈ s)) : (factors C s x).prod = spanFinBasis C s x :=
  by
  ext y
  dsimp [spanFinBasis]
  split_ifs with h <;> [exact factors_prod_eq_basis_of_eq _ _ h; exact factors_prod_eq_basis_of_ne _ _ h]

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