coord_reindex

Mathlib.LinearAlgebra.AffineSpace.Basis

URI: https://scilib.ai/kg/mathlib#AffineBasis.coord_reindex

English

The index type ι is nonempty; equivalently, an affine basis exists only if ι is nonempty.

Русский

Тип индексов ι непуст; следовательно, аффинный базис существует только если ι непуст.

LaTeX

$$$\operatorname{Nonempty} ι$$$

Lean4

@[simp]
theorem coord_reindex (i : ι') : (b.reindex e).coord i = b.coord (e.symm i) :=
  by
  ext
  classical simp [AffineBasis.coord]

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

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

Разделы

Аффилиация

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