Theorems · Theorem · order theory
Nat.card_Ico
∀ (a b : ℕ), (Finset.Ico a b).card = b - a
- Defined in
- Mathlib.Order.Interval.Finset.Nat
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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.Icostatement · cited by 450
Cited by19
Results whose statement or proof uses this declaration.
- Nat.card_Iioproof · cited by 4
- Nat.factorization_choose_le_logproof · cited by 3
- Nat.Prime.emultiplicity_choose_prime_pow_add_emultiplicityproof · cited by 2
- Finset.le_sum_schlomilch'proof · cited by 2
- Finset.sum_schlomilch_le'proof · cited by 2
- AkraBazziRecurrence.eventually_atTop_sumTransform_geproof · cited by 1
- AkraBazziRecurrence.eventually_atTop_sumTransform_leproof · cited by 1
- Nat.emultiplicity_eq_card_pow_dvdproof · cited by 1
- PNat.card_Icoproof · cited by 1
- Nat.card_divisors_le_selfproof · cited by 1
- Nat.factorization_choose_prime_pow_add_factorizationproof · cited by 1
- Nat.totient_eq_iff_primeproof · cited by 1