Mathlib Map

Theorems · Theorem · logic and foundations

Nat.card_sigma

∀ {α : Type u_1} {β : α → Type u_3} [inst : Fintype α] [∀ (a : α), Finite (β a)],
  Nat.card (Sigma β) = ∑ a, Nat.card (β a)
Defined in
Mathlib.SetTheory.Cardinal.Finite
Cited by
1 results in Mathlib
Foundations
Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FintypeFinite
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

IsGalois.of_separable_splitting_field_aux · cited by 0IsGalois.of_separable_spl…Fintype · cited by 7736FintypeFinset.sum · cited by 5195Finset.sumFinset.univ · cited by 3473Finset.univFinite · cited by 3029FiniteFinset.sum_congr · cited by 2323Finset.sum_congrFintype.card · cited by 1386Fintype.cardNat.card · cited by 844Nat.cardFintype.ofFinite · cited by 255Fintype.ofFiniteNat.card_eq_fintype_card · cited by 200Nat.card_eq_fintype_cardFintype.card_sigma · cited by 14Fintype.card_sigmaNat.card_sigmaCITED BYCITES

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.