constVAdd_zero

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

URI: https://scilib.ai/kg/mathlib#AffineEquiv.constVAdd_zero

English

The map constVAdd with zero vector is the identity on the affine space: constVAdd k P1 0 = AffineEquiv.refl k P1.

Русский

Отображение constVAdd на нулевом векторе даёт тождество: constVAdd k P1 0 = AffineEquiv.refl k P1.

LaTeX

$$$\mathrm{constVAdd}_k(P_1,0) = \mathrm{refl}_{k} P_1$$$

Lean4

@[simp]
theorem constVAdd_zero : constVAdd k P₁ 0 = AffineEquiv.refl _ _ :=
  ext <| zero_vadd _

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

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

Разделы

Аффилиация

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