forall — Mathlib

English

For every list l and every natural number n, the rotated version l.rotate n is a rotation of l.

Русский

Для каждого списка l и любого натурального числа n поворот l.rotate n является вращением l.

LaTeX

$$$ \forall l:\text{List}, \forall n:\mathbb{N}, \ (l \rotate n) \sim_{\mathrm{rot}} l $$$

Lean4

@[simp]
protected theorem «forall» (l : List α) (n : ℕ) : l.rotate n ~r l :=
  IsRotated.symm ⟨n, rfl⟩

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