Vars — Mathlib

English

Vars k is the indexing set for the indeterminates X_{f,i} attached to each monic f of k[X], with i ranging over the degree of f.

Русский

Vars k — множество индексов для независимых переменных X_{f,i} привязанных к каждому моническому f над k[X], где i пробегает по степени f.

LaTeX

$$$\\mathrm{Vars}(k) = \\Sigma f : \\mathrm{Monics}(k), \\; \\mathrm{Fin}(f.1.natDegree)$$$

Lean4

/-- `Vars k` provides `n` variables $X_{f,1}, \dots, X_{f,n}$ for each monic polynomial
`f : k[X]` of degree `n`. -/
def Vars : Type u :=
  Σ f : Monics k, Fin f.1.natDegree

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