Theorems · Theorem · group theory

Equiv.Perm.cycle_induction_on

∀ {β : Type u_3} [Finite β] (P : Equiv.Perm β → Prop) (σ : Equiv.Perm β),
  P 1 →
    (∀ (σ : Equiv.Perm β), σ.IsCycle → P σ) →
      (∀ (σ τ : Equiv.Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)) → P σ

Defined in

Mathlib.GroupTheory.Perm.Cycle.Factors

Cited by

8 results in Mathlib

Foundations

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

Assumes

Finite