basisOf_apply

Mathlib.LinearAlgebra.AffineSpace.Basis

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

English

The j-th element of basisOf i equals b j −ᵥ b i.

Русский

j-й элемент_basisOf i равен b_j −ᵥ b_i.

LaTeX

$$$(b.basisOf i) j = b j -ᵥ b i$$$

Lean4

@[simp]
theorem basisOf_apply (i : ι) (j : { j : ι // j ≠ i }) : b.basisOf i j = b ↑j -ᵥ b i := by simp [basisOf]

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

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

Разделы

Аффилиация

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