constVAdd_symm

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

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

English

The inverse of translating by v is translating by -v.

Русский

Обратный перенос по вектору v равен переносу по -v.

LaTeX

$$$T_v^{-1} = T_{-v}$$$

Lean4

@[simp]
theorem constVAdd_symm (v : V₁) : (constVAdd k P₁ v).symm = constVAdd k P₁ (-v) :=
  ext fun _ => rfl

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

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

Разделы

Аффилиация

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