constVAdd_zsmul

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

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

English

For any integer z, translation by z*v equals z-th power of translation by v.

Русский

Для целого z перенос на z*v равен z-ой степени переноса на v.

LaTeX

$$T_{z\,v} = T_v^z$$

Lean4

theorem constVAdd_zsmul (z : ℤ) (v : V₁) : constVAdd k P₁ (z • v) = constVAdd k P₁ v ^ z :=
  (constVAddHom k P₁).map_zpow _ _

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

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

Разделы

Аффилиация

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