Commit 2026-07-15 14:47 28313485

View on Github →

chore(Data/Finsupp): rename mapDomain_notin_range to mapDomain_of_notMem_range (#41766) ... so that this follows the naming convention. Same for embDomain and for HahnSeries.

Estimated changes

Modified Mathlib/Algebra/Group/Finsupp.lean

Modified Mathlib/Analysis/InnerProductSpace/SingularValues.lean

Modified Mathlib/Combinatorics/Nullstellensatz.lean

Modified Mathlib/Data/Finsupp/Basic.lean

deleted theorem Finsupp.mapDomain_notin_range

added theorem Finsupp.mapDomain_of_notMem_range

Modified Mathlib/Data/Finsupp/Defs.lean

deleted theorem Finsupp.embDomain_notin_range

added theorem Finsupp.embDomain_of_notMem_range

Modified Mathlib/Data/Finsupp/Option.lean

Modified Mathlib/Data/Finsupp/Order.lean

Modified Mathlib/Data/Finsupp/Sigma.lean

Modified Mathlib/Data/List/ToFinsupp.lean

Modified Mathlib/RingTheory/Extension/Generators.lean

Modified Mathlib/RingTheory/HahnSeries/Addition.lean

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

deleted theorem HahnSeries.embDomain_notin_range

added theorem HahnSeries.embDomain_of_notMem_range

Modified Mathlib/RingTheory/HahnSeries/Lex.lean

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

deleted theorem HahnSeries.SummableFamily.embDomain_notin_range

added theorem HahnSeries.SummableFamily.embDomain_of_notMem_range

Modified Mathlib/RingTheory/IsAdjoinRoot.lean

Modified Mathlib/RingTheory/LaurentSeries.lean