Theorems · Theorem · combinatorics
Finset.singleton_product
∀ {α : Type u_1} {β : Type u_2} {t : Finset β} {a : α}, {a} ×ˢ t = Finset.map { toFun := Prod.mk a, inj' := ⋯ } t- Defined in
- Mathlib.Data.Finset.Prod
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- SProd.sprodstatement · cited by 1,750
- Finset.mapstatement · cited by 747
- Finset.extproof · cited by 565
- Prod.mk_right_injectivestatement · cited by 15
Cited by8
Results whose statement or proof uses this declaration.
- Multiset.map_toEnumFinset_fstproof · cited by 7
- Multiset.map_fst_le_of_subset_toEnumFinsetproof · cited by 3
- PairReduction.card_pairSetSeq_le_logSizeRadius_mulproof · cited by 1
- PairReduction.edist_le_of_mem_pairSetproof · cited by 1
- PairReduction.iSup_edist_pairSetproof · cited by 1
- Multiset.toEnumFinset_filter_eqproof · cited by 1
- YoungDiagram.mem_cellsOfRowLensproof · cited by 1
- YoungDiagram.rowLen_eq_cardproof · cited by 0