basis_apply — Mathlib

English

If f is monic and S is an algebra over R with IsAdjoinRootMonic S f, then the basis for S as an R-module is given by powers of the root: the i-th basis element equals the root raised to i.

Русский

Пусть f является моноичным и S — кольцо над R с IsAdjoinRootMonic S f; тогда базис S как модуля над R задаётся степенями корня: i-й элемент базиса равен корню в степени i.

LaTeX

$$$ h.basis i = h.root^{(i : \\mathbb{N})} $$$

Lean4

@[simp]
theorem basis_apply (i) : h.basis i = h.root ^ (i : ℕ) :=
  Basis.apply_eq_iff.mpr <| by simp [IsAdjoinRootMonic.basis]

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