rotate_rotate

Mathlib.GroupTheory.Perm.Cycle.Type

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.VectorsProdEqOne.rotate_rotate

English

Applying two rotations is equivalent to a single rotation by the sum of the shifts.

Русский

Применение двух поворотов эквивалентно повороту на сумму смещений.

LaTeX

$$rotate (rotate v j) k = rotate v (j + k)$$

Lean4

theorem rotate_rotate : rotate (rotate v j) k = rotate v (j + k) :=
  Subtype.ext (Subtype.ext (v.1.1.rotate_rotate j k))

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

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

Разделы

Аффилиация

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