basisOf_vadd

Mathlib.LinearAlgebra.AffineSpace.Basis

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

English

Translating an affine basis by a vector v does not change its basisOf set: (v +ᵥ b).basisOf = b.basisOf.

Русский

Перенос аффинной базы на вектор v не изменяет её множество базовых векторов: (v +ᵥ b).basisOf = b.basisOf.

LaTeX

$$(v +ᵥ b).basisOf = b.basisOf$$

Lean4

@[simp]
theorem basisOf_vadd (v : V) (b : AffineBasis ι k P) : (v +ᵥ b).basisOf = b.basisOf :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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