indicator — Mathlib

English

Over a field, the indicator is the product of factors encoding evaluation at the chosen field elements.

Русский

Над полем индикатор — это произведение фактороp, кодирующее значения по элементам поля.

LaTeX

$$indicator [CommRing K] (a : σ → K) = ∏ n (1 - (X n - C (a n))^{|K| - 1})$$

Lean4

/-- Over a field, this is the indicator function as an `MvPolynomial`. -/
def indicator [CommRing K] (a : σ → K) : MvPolynomial σ K :=
  ∏ n, (1 - (X n - C (a n)) ^ (Fintype.card K - 1))

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