Theorems · Definition · combinatorics
Fin.consEquiv
{n : ℕ} → (α : Fin (n + 1) → Type u_1) → α 0 × ((i : Fin n) → α i.succ) ≃ ((i : Fin (n + 1)) → α i)Equivalence between tuples of length n + 1 and pairs of an element and a tuple of length n
given by separating out the first element of the tuple.
This is Fin.cons as an Equiv.
- Defined in
- Mathlib.Data.Fin.Tuple.Basic
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 34 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by24
Results whose statement or proof uses this declaration.
- groupHomology.chainsIso₃proof · cited by 15
- groupCohomology.cochainsIso₃proof · cited by 11
- groupHomology.comp_d₃₂_eqproof · cited by 6
- Action.diagonalSuccIsoTensorDiagonalproof · cited by 5
- groupCohomology.comp_d₂₃_eqproof · cited by 5
- Fin.consOrderIsoproof · cited by 4
- Fin.insertNthEquiv_zerostatement and proof · cited by 3
- groupHomology.chainsMap_f_3_comp_chainsIso₃proof · cited by 2
- groupCohomology.cochainsMap_f_3_comp_cochainsIso₃proof · cited by 2
- Fin.consEquiv_applystatement and proof · cited by 2
- Fin.consEquiv_symm_applystatement and proof · cited by 2
- Fin.consLinearEquivproof · cited by 2