Theorems · Theorem · group theory
Finset.card_eq_sum_ones
∀ {ι : Type u_1} (s : Finset ι), s.card = ∑ x ∈ s, 1- Cited by
- 22 results in Mathlib
- Foundations
- Depth 23 from the axioms · uses propext, 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
- Finset.sumstatement · cited by 5,195
- mul_oneproof · cited by 3,885
- Finset.cardstatement and proof · cited by 2,327
- Finset.sum_constproof · cited by 254
Cited by22
Results whose statement or proof uses this declaration.
- ZMod.card_units_eq_totientproof · cited by 15
- Finset.card_eq_sum_card_fiberwiseproof · cited by 11
- NumberField.InfinitePlace.sum_mult_eqproof · cited by 7
- Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelowproof · cited by 5
- Lagrange.natDegree_basisproof · cited by 3
- Matrix.charpoly_sub_diagonal_degree_ltproof · cited by 3
- char_dvd_card_solutions_of_sum_ltproof · cited by 2
- SimpleGraph.Walk.IsHamiltonian.length_eqproof · cited by 2
- Finset.le_sum_card_interproof · cited by 2
- NumberField.InfinitePlace.card_complex_embeddingsproof · cited by 2
- Finset.sum_card_fiberwise_eq_card_filterproof · cited by 2
- Finset.sum_card_inter_leproof · cited by 2