Commit 2026-09-29 11:08 1b5006ca

View on Github →

chore: rename remaining not_mem declarations to notMem (#44296) Renames the remaining declarations whose not_mem stands for ∉ in their statement to notMem, and the Finset.not_mem_subset alias to Finset.notMem_subset.

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/MapDomain.lean

added theorem MonoidAlgebra.comapDomain_single_of_notMem_range

deleted theorem MonoidAlgebra.comapDomain_single_of_not_mem_range

Modified Mathlib/Combinatorics/Hypergraph/Basic.lean

added theorem Hypergraph.IsTrivial.notMem_edgeSet

deleted theorem Hypergraph.IsTrivial.not_mem_edgeSet

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

added theorem SimpleGraph.notMem_edgeSet_of_isDiag

deleted theorem SimpleGraph.not_mem_edgeSet_of_isDiag

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

added theorem SimpleGraph.Walk.IsTrail.notMem_edges_of_not_reachable

added theorem SimpleGraph.Walk.IsTrail.notMem_support_of_not_reachable

added theorem SimpleGraph.Walk.IsTrail.notMem_support_of_subsingleton_neighborSet

deleted theorem SimpleGraph.Walk.IsTrail.not_mem_edges_of_not_reachable

deleted theorem SimpleGraph.Walk.IsTrail.not_mem_support_of_not_reachable

deleted theorem SimpleGraph.Walk.IsTrail.not_mem_support_of_subsingleton_neighborSet

Modified Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

Modified Mathlib/Data/Finset/Defs.lean

Modified Mathlib/Data/Finset/Option.lean

added theorem Finset.card_eraseNone_of_notMem

deleted theorem Finset.card_eraseNone_of_not_mem

Modified Mathlib/Data/Finsupp/Basic.lean

added theorem Finsupp.comapDomain_single_of_notMem_range

deleted theorem Finsupp.comapDomain_single_of_not_mem_range

added theorem Finsupp.mapDomain_of_notMem_image_support

deleted theorem Finsupp.mapDomain_of_not_mem_image_support

Modified Mathlib/Data/List/Lattice.lean

added theorem List.bagInter_cons_of_notMem

deleted theorem List.bagInter_cons_of_not_mem

added theorem List.bagInter_erase_of_notMem

deleted theorem List.bagInter_erase_of_not_mem

added theorem List.cons_bagInter_of_notMem

deleted theorem List.cons_bagInter_of_not_mem

added theorem List.erase_bagInter_of_notMem

deleted theorem List.erase_bagInter_of_not_mem

Modified Mathlib/Data/Multiset/UnionInter.lean

Modified Mathlib/Data/Set/Card.lean

added theorem Finset.exists_notMem_of_card_lt_enatCard

deleted theorem Finset.exists_not_mem_of_card_lt_enatCard

Modified Mathlib/Data/SetLike/Basic.lean

added theorem SetLike.exists_notMem_of_ne_top

deleted theorem SetLike.exists_not_mem_of_ne_top

Modified Mathlib/Geometry/Convex/ConvexSpace/Defs.lean

Modified Mathlib/Geometry/Convex/Set.lean

Modified Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean

added theorem SubMulAction.notMem_of_mem_ofFixingSubgroup

deleted theorem SubMulAction.not_mem_of_mem_ofFixingSubgroup

Modified Mathlib/InformationTheory/Coding/KraftMcMillan.lean

Modified Mathlib/InformationTheory/Coding/UniquelyDecodable.lean

added theorem InformationTheory.IsUniquelyDecodable.epsilon_notMem

deleted theorem InformationTheory.IsUniquelyDecodable.epsilon_not_mem

Modified Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean

added theorem LinearIndependent.finSnoc_of_notMem_span_over

deleted theorem LinearIndependent.finSnoc_of_not_mem_span_over

Modified Mathlib/LinearAlgebra/Transvection/Basic.lean

Modified Mathlib/MeasureTheory/Measure/Dirac/Basic.lean

added theorem MeasureTheory.dirac_eq_zero_iff_notMem

deleted theorem MeasureTheory.dirac_eq_zero_iff_not_mem

Modified Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean

added theorem IsCyclotomicExtension.Rat.two_notMem_span_zeta_sub_one'

deleted theorem IsCyclotomicExtension.Rat.two_not_mem_span_zeta_sub_one'

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

added theorem not_dvd_differentIdeal_of_intTrace_notMem

deleted theorem not_dvd_differentIdeal_of_intTrace_not_mem

Modified Mathlib/RingTheory/DividedPowers/RatAlgebra.lean

added theorem DividedPowers.OfInvertibleFactorial.dpow_eq_of_notMem

deleted theorem DividedPowers.OfInvertibleFactorial.dpow_eq_of_not_mem

Modified Mathlib/RingTheory/Etale/QuasiFinite.lean

Modified Mathlib/RingTheory/QuasiFinite/Basic.lean

added theorem Ideal.exists_notMem_forall_mem_of_ne_of_liesOver

deleted theorem Ideal.exists_not_mem_forall_mem_of_ne_of_liesOver

Modified Mathlib/RingTheory/Spectrum/Prime/Noetherian.lean

added theorem IsArtinianRing.exists_notMem_forall_mem_of_ne

deleted theorem IsArtinianRing.exists_not_mem_forall_mem_of_ne

Modified Mathlib/RingTheory/Unramified/LocalStructure.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Defs.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/SummationFilter.lean

added theorem SummationFilter.eventually_mem_or_notMem

deleted theorem SummationFilter.eventually_mem_or_not_mem

Modified Mathlib/Topology/CWComplex/Classical/Subcomplex.lean

added theorem Topology.RelCWComplex.Subcomplex.disjoint_openCell_subcomplex_of_notMem

deleted theorem Topology.RelCWComplex.Subcomplex.disjoint_openCell_subcomplex_of_not_mem