Theorems · Theorem · group theory
Fin.cons_apply_cycleRange
∀ {n : ℕ} {α : Type u_1} (a : α) (x : Fin n → α) (p j : Fin (n + 1)), Fin.cons a x (p.cycleRange j) = p.insertNth a x j- Defined in
- Mathlib.GroupTheory.Perm.Fin
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- Equiv.Permstatement · cited by 1,375
- Equiv.symm_apply_applyproof · cited by 320
- Fin.consstatement · cited by 190
- Fin.insertNthstatement and proof · cited by 95
- Fin.cycleRangestatement and proof · cited by 35
- Fin.insertNth_apply_cycleRange_symmproof · cited by 2
Cited by1
Results whose statement or proof uses this declaration.
- Fin.cons_comp_cycleRangeproof · cited by 1