Theorems · Theorem · group theory

Equiv.Perm.disjoint_ofSubtype_noncommPiCoprod

∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α)
  (u : Equiv.Perm ↑(Function.fixedPoints ⇑f)) (v : (c : ↥f.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)),
  (Equiv.Perm.ofSubtype u).Disjoint ((Subgroup.noncommPiCoprod ⋯) v)

Defined in: Mathlib.GroupTheory.Perm.Cycle.Factors
Cited by: 2 results in Mathlib
Foundations: Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DecidableEq Fintype

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites25

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setstatement · cited by 53,352
Finsetstatement · cited by 13,712
SetLike.coeproof · cited by 8,199
Fintypestatement and proof · cited by 7,736
Set.Elemstatement and proof · cited by 7,166
MonoidHomstatement · cited by 3,629
Subgroupstatement · cited by 3,593
Finset.univproof · cited by 3,473
le_rflproof · cited by 1,558
Equiv.Permstatement and proof · cited by 1,375
Subgroup.zpowersstatement and proof · cited by 204

Cited by2

Results whose statement or proof uses this declaration.

Equiv.Perm.commute_ofSubtype_noncommPiCoprodproof · cited by 5
Equiv.Perm.OnCycleFactors.cycleType_kerParam_apply_applyproof · cited by 0