Mathlib Map

Theorems · Theorem · combinatorics

Multiset.zero_add

∀ {α : Type u_1} (s : Multiset α), 0 + s = s
Defined in
Mathlib.Data.Multiset.AddSub
Cited by
15 results in Mathlib
Foundations
Depth 14 from the axioms · uses Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Multiset.le_add_left · cited by 6Multiset.le_add_leftMultiset.filter_cons · cited by 5Multiset.filter_consMultiset.filterMap_cons · cited by 2Multiset.filterMap_consMultiset.zero_union · cited by 2Multiset.zero_unionPolynomial.roots_quadratic_eq_pair_iff_of_ne_zero · cited by 2Polynomial.roots_quadrati…Finset.empty_disjUnion · cited by 1Finset.empty_disjUnionMultiset.nodup_iff_ne_cons_cons · cited by 1Multiset.nodup_iff_ne_con…Multiset.rel_add_left · cited by 1Multiset.rel_add_leftMultiset.Rel.add · cited by 1Rel.addMultiset.esymm_pair_two · cited by 1Multiset.esymm_pair_twoMultiset.multinomial_add · cited by 1Multiset.multinomial_addMultiset.zero_disjSum · cited by 1Multiset.zero_disjSumMultiset.sections_add · cited by 0Multiset.sections_addMultiset.powersetCard_self · cited by 0Multiset.powersetCard_selfMultiset.antidiagonal_add · cited by 0Multiset.antidiagonal_addMultiset · cited by 2627MultisetMultiset.zero_addCITED BYCITES

Cites1

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

Cited by15

Results whose statement or proof uses this declaration.