Commit 2026-05-13 14:16 03cc2f9c

View on Github →

feat(Data): lemmas for List.bagInter (#35892) Basic API lemmas for List.bagInter and correct a few misnamed lemmas.

Estimated changes

Modified Mathlib/Data/List/Lattice.lean

added theorem List.Nodup.bagInter_left

added theorem List.Nodup.bagInter_right

added theorem List.Sublist.bagInter_inter

added theorem List.Sublist.inter_left

added theorem List.Sublist.inter_right

added theorem List.bagInter_cons_of_not_mem

added theorem List.bagInter_eq_nil_iff_disjoint

added theorem List.bagInter_erase_of_not_mem

added theorem List.bagInter_singleton

deleted theorem List.cons_bagInteger

added theorem List.cons_bagInter

added theorem List.cons_bagInter_of_mem

deleted theorem List.cons_bagInter_of_neg

added theorem List.cons_bagInter_of_not_mem

deleted theorem List.cons_bagInter_of_pos

added theorem List.erase_bagInter_of_not_mem

added theorem List.singleton_bagInter

Modified Mathlib/Data/List/Perm/Lattice.lean

added theorem List.Perm.bagInter_symm

Modified Mathlib/Data/Multiset/UnionInter.lean