Theorems · Theorem · combinatorics
Multiset.card_cons
∀ {α : Type u_1} (a : α) (s : Multiset α), (a ::ₘ s).card = s.card + 1- Defined in
- Mathlib.Data.Multiset.ZeroCons
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses propext, 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.
- Multisetstatement and proof · cited by 2,627
- Multiset.cardstatement · cited by 375
- Multiset.consstatement · cited by 313
Cited by19
Results whose statement or proof uses this declaration.
- Multiset.card_singletonproof · cited by 17
- Finset.card_consproof · cited by 16
- Equiv.Perm.sign_of_cycleTypeproof · cited by 7
- Multiset.card_pairproof · cited by 6
- Multiset.card_eq_card_of_relproof · cited by 5
- Equiv.Perm.closure_cycleType_eq_two_two_eq_alternatingGroupproof · cited by 2
- UniqueFactorizationMonoid.card_factors_of_irreducibleproof · cited by 2
- isAddFreimanHom_antitoneproof · cited by 1
- Equiv.Perm.cycleType_eq_two_two_subset_alternatingGroupproof · cited by 1
- Ideal.pow_multiset_sum_mem_span_powproof · cited by 1
- ADEInequality.admissible_of_one_lt_sumInvproof · cited by 1
- Multiset.covBy_consproof · cited by 1