rotate — Mathlib

English

Rotation of a vectorsProdEqOne element preserves the product 1 and moves positions cyclically.

Русский

Поворот элемента vectorsProdEqOne сохраняет произведение 1 и циклически сдвигает позиции.

LaTeX

$$rotate : vectorsProdEqOne G n → Nat → vectorsProdEqOne G n$$

Lean4

/-- Rotate a vector whose product is 1. -/
def rotate : vectorsProdEqOne G n :=
  ⟨⟨_, (v.1.1.length_rotate k).trans v.1.2⟩, List.prod_rotate_eq_one_of_prod_eq_one v.2 k⟩

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