Theorems · Theorem · combinatorics
Finset.card_range
∀ (n : ℕ), (Finset.range n).card = n
- Defined in
- Mathlib.Data.Finset.Card
- Cited by
- 108 results in Mathlib
- Foundations
- Depth 54 from the axioms, rests on 753 definitions · uses propext, Classical.choice, 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.
- Finset.cardstatement · cited by 2,327
- Finset.rangestatement · cited by 1,341
- Multiset.card_rangeproof · cited by 5
Cited by108
Results whose statement or proof uses this declaration.
- ENNReal.tsum_geometricproof · cited by 8
- Int.card_Iccproof · cited by 6
- Int.card_Icoproof · cited by 6
- IsCoprime.pow_leftproof · cited by 5
- Infinite.exists_subset_card_eqproof · cited by 5
- Int.card_Iocproof · cited by 5
- Nat.totient_prime_pow_succproof · cited by 4
- Set.Infinite.exists_subset_card_eqproof · cited by 4
- Finset.pow_eq_prod_constproof · cited by 4
- IsCoprime.pow_left_iffproof · cited by 4
- Polynomial.eval_one_cyclotomic_prime_powproof · cited by 4
- MonovaryOn.sum_smul_sum_le_card_smul_sumproof · cited by 4