basis — Mathlib

English

The coordinate ring basis evaluated at n is equal to the generator raised to the n-th power, i.e., basis W' at n equals gen^n.

Русский

Основание координатного кольца, взятое в позиции n, равно генератору в степени n: basis W' n = gen^n.

LaTeX

$$$ CoordinateRing.basis W' n = (AdjoinRoot.powerBasis' monic_polynomial).gen^{(n : \mathbb{N})} $$$

Lean4

/-- The power basis `{1, Y}` for `R[W]` over `R[X]`. -/
protected noncomputable def basis : Basis (Fin 2) R[X] W'.CoordinateRing :=
  (subsingleton_or_nontrivial R).by_cases (fun _ => default) fun _ =>
    (AdjoinRoot.powerBasis' monic_polynomial).basis.reindex <| finCongr natDegree_polynomial

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