Theorems · Theorem · group theory

Equiv.Perm.IsCycle.eq_on_support_inter_nonempty_congr

∀ {α : Type u_2} {f g : Equiv.Perm α} {x : α} [inst : DecidableEq α] [inst_1 : Fintype α],
  f.IsCycle → g.IsCycle → (∀ x ∈ f.support ∩ g.support, f x = g x) → f x = g x → x ∈ f.support → f = g

If two cyclic permutations agree on all terms in their intersection, and that intersection is not empty, then the two cyclic permutations must be equal.

Defined in

Mathlib.GroupTheory.Perm.Cycle.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqFintype