Theorems · Theorem · combinatorics
Configuration.sum_lineCount_eq_sum_pointCount
∀ (P : Type u_1) (L : Type u_2) [inst : Membership P L] [inst_1 : Fintype P] [inst_2 : Fintype L], ∑ p, Configuration.lineCount L p = ∑ l, Configuration.pointCount P l
- Defined in
- Mathlib.Combinatorics.Configuration
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MembershipFintypeFintype
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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 and proof · cited by 5,195
- Equiv.symmproof · cited by 3,681
- Finset.univstatement and proof · cited by 3,473
- Nat.card_eq_fintype_cardproof · cited by 200
- Fintype.card_congrproof · cited by 67
- Equiv.prodCommproof · cited by 55
- Equiv.subtypeEquivproof · cited by 32
- Configuration.lineCountstatement · cited by 11
- Configuration.pointCountstatement · cited by 11
- Equiv.subtypeProdEquivSigmaSubtypeproof · cited by 2
Cited by3
Results whose statement or proof uses this declaration.
- Configuration.HasLines.lineCount_eq_pointCountproof · cited by 3
- Configuration.HasLines.card_leproof · cited by 2
- Configuration.HasLines.exists_bijective_of_card_eqproof · cited by 1