Theorems · Definition · combinatorics
piFinTwoEquiv
(α : Fin 2 → Type u) → ((i : Fin 2) → α i) ≃ α 0 × α 1
Π i : Fin 2, α i is equivalent to α 0 × α 1. See also finTwoArrowEquiv for a
non-dependent version and prodEquivPiFinTwo for a version with inputs α β : Type u.
- Defined in
- Mathlib.Data.Fin.Tuple.Basic
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 33 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.
- Equivstatement · cited by 8,337
- Fin.consproof · cited by 190
- finZeroElimproof · cited by 29
Cited by32
Results whose statement or proof uses this declaration.
- groupHomology.chainsIso₂proof · cited by 32
- groupCohomology.cochainsIso₂proof · cited by 28
- groupHomology.chainsIso₃proof · cited by 15
- groupCohomology.cochainsIso₃proof · cited by 11
- finTwoArrowEquivproof · cited by 10
- groupHomology.comp_d₂₁_eqproof · cited by 10
- groupCohomology.comp_d₁₂_eqproof · cited by 10
- piFinTwoEquiv_applystatement and proof · cited by 9
- groupHomology.comp_d₃₂_eqproof · cited by 6
- MeasurableEquiv.piFinTwoproof · cited by 6
- groupCohomology.comp_d₂₃_eqproof · cited by 5
- groupCohomology.cochainsMap_f_2_comp_cochainsIso₂proof · cited by 4