Theorems · Theorem · group theory
Multiset.sum_singleton
∀ {M : Type u_3} [inst : AddCommMonoid M] (a : M), {a}.sum = a- Cited by
- 26 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext, Quot.sound
- Assumes
- AddCommMonoid
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.
- AddCommMonoidstatement and proof · cited by 12,281
- add_zeroproof · cited by 2,707
- Multisetstatement · cited by 2,627
- Multiset.sumstatement · cited by 388
- Multiset.sum_consproof · cited by 45
Cited by26
Results whose statement or proof uses this declaration.
- Equiv.Perm.sum_cycleTypeproof · cited by 14
- Equiv.Perm.IsThreeCycle.card_supportproof · cited by 6
- Polynomial.iterate_derivative_mulproof · cited by 4
- ADEInequality.sumInv_pqrproof · cited by 4
- card_support_eq_three_iffproof · cited by 3
- Multiset.sum_pairproof · cited by 2
- Equiv.Perm.closure_cycleType_eq_two_two_eq_alternatingGroupproof · cited by 2
- Equiv.Perm.isSwap_iff_cycleTypeproof · cited by 2
- Equiv.Perm.card_of_cycleType_singletonproof · cited by 1
- Multiset.esymm_pair_oneproof · cited by 1
- Multiset.esymm_pair_twoproof · cited by 1
- Equiv.Perm.cycleType_eq_two_two_subset_alternatingGroupproof · cited by 1