basis_apply — Mathlib

English

The basis at index 0 equals 1 in the coordinate ring.

Русский

База на нулевом индексе равна единице в координатном кольце.

LaTeX

$$$ CoordinateRing.basis W' 0 = 1 $$$

Lean4

theorem basis_apply (n : Fin 2) : CoordinateRing.basis W' n = (AdjoinRoot.powerBasis' monic_polynomial).gen ^ (n : ℕ) :=
  by
  classical
  nontriviality R
  rw [CoordinateRing.basis, Or.by_cases, dif_neg <| not_subsingleton R, Basis.reindex_apply, PowerBasis.basis_eq_pow,
    finCongr_symm_apply, Fin.coe_cast]

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