length — Mathlib

English

The length of a cycle is the length of any representative list; more precisely, for any l, length(Cycle.ofList l) = length(l).

Русский

Длина цикла равна длине любого репрезентативного списка; точнее, для любого списка l выполняется length(Cycle.ofList l) = length(l).

LaTeX

$$$\text{length}(\text{Cycle.ofList}(l)) = \text{length}(l)$$$

Lean4

/-- The length of the `s : Cycle α`, which is the number of elements, counting duplicates. -/
def length (s : Cycle α) : ℕ :=
  Quot.liftOn s List.length fun _ _ e => e.perm.length_eq

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