algebraMapCoeffs_apply

Mathlib.RingTheory.AlgebraTower

URI: https://scilib.ai/kg/mathlib#Module.Basis.algebraMapCoeffs_apply

English

For each index i, the i-th coefficient of the algebra-map basis equals the i-th basis element.

Русский

Для каждого индекса i коэффициент i-го элемента алгебраMap-образной базы равен i-му элементу базы.

LaTeX

$$$$ (b.algebraMapCoeffs A h) i = b i $$$$

Lean4

theorem algebraMapCoeffs_apply (i : ι) : b.algebraMapCoeffs A h i = b i :=
  b.mapCoeffs_apply _ _ _

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

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

Разделы

Аффилиация

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