Theorems · Definition · group theory

Equiv.Perm.toList

{α : Type u_1} → [Fintype α] → [DecidableEq α] → Equiv.Perm α → α → List α

Equiv.Perm.toList (f : Perm α) (x : α) generates the list [x, f x, f (f x), ...] until looping. That means when f x = x, toList f x = [].

Defined in

Mathlib.GroupTheory.Perm.Cycle.Concrete

Cited by

24 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableEq