constVAdd_nsmul

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

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

English

Translation by n times v equals the nth power of translation by v.

Русский

Перенос на n*v равен n-ой степенью переноса на v.

LaTeX

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

Lean4

theorem constVAdd_nsmul (n : ℕ) (v : V₁) : constVAdd k P₁ (n • v) = constVAdd k P₁ v ^ n :=
  (constVAddHom k P₁).map_pow _ _

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

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

Разделы

Аффилиация

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