coe_basis

Mathlib.RingTheory.PowerBasis

URI: https://scilib.ai/kg/mathlib#PowerBasis.coe_basis

English

The basis of a power basis pb.basis corresponds to pb.gen via pb.gen^i for i from Fin pb.dim.

Русский

Пусть pb.basis выражает основание, тогда pb.basis i = pb.gen^{i} для i из Fin(pb.dim).

LaTeX

$$$\\text{coe}_{\\mathsf{Basis}}(pb) : \\text{basis} = (i \\mapsto pb.gen^{(i : \\mathbb{N})})$$$

Lean4

@[simp]
theorem coe_basis (pb : PowerBasis R S) : ⇑pb.basis = fun i : Fin pb.dim => pb.gen ^ (i : ℕ) :=
  funext pb.basis_eq_pow

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru