Theorems · Theorem · combinatorics
Fintype.card_sigma
∀ {ι : Type u_8} {α : ι → Type u_7} [inst : Fintype ι] [inst_1 : (i : ι) → Fintype (α i)],
Fintype.card (Sigma α) = ∑ i, Fintype.card (α i)- Defined in
- Mathlib.Data.Fintype.BigOperators
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 67 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.
- Fintypestatement and proof · cited by 7,736
- Finset.sumstatement · cited by 5,195
- Finset.univstatement and proof · cited by 3,473
- Fintype.cardstatement · cited by 1,386
- Finset.card_sigmaproof · cited by 2
Cited by14
Results whose statement or proof uses this declaration.
- Module.finrank_pi_fintypeproof · cited by 6
- IsPGroup.card_modEq_card_fixedPointsproof · cited by 4
- Subgroup.index_eq_sum_minimalPeriodproof · cited by 3
- Module.finrank_directSumproof · cited by 2
- card_comm_eq_card_conjClasses_mul_cardproof · cited by 2
- card_linearIndependentproof · cited by 1
- MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_groupproof · cited by 1
- Fintype.card_embedding_eqproof · cited by 1
- sum_conjClasses_card_eq_cardproof · cited by 1
- Configuration.ProjectivePlane.card_pointsproof · cited by 1
- Nat.card_sigmaproof · cited by 1
- card_derangements_fin_add_twoproof · cited by 1