Commit 2025-04-03 00:00 ecdddd70

View on Github →

chore: fix missing namespaces (#23565) Deprecations aren't viable here because they cause name ambiguities with the new name, which would result in an error. Moves:

mem_span_range_iff_exists_fun → Submodule.mem_span_range_iff_exists_fun
top_le_span_range_iff_forall_exists_fun → Submodule.top_le_span_range_iff_forall_exists_fun
mem_span_image_iff_exists_fun → Submodule.mem_span_image_iff_exists_fun
mem_span_set → Submodule.mem_span_set
mem_span_set' → Submodule.mem_span_set'
span_eq_iUnion_nat → Submodule.span_eq_iUnion_nat

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

Modified Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean

Modified Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean

added theorem Submodule.mem_span_image_iff_exists_fun

added theorem Submodule.mem_span_range_iff_exists_fun

added theorem Submodule.mem_span_set'

added theorem Submodule.mem_span_set

added theorem Submodule.span_eq_iUnion_nat

added theorem Submodule.top_le_span_range_iff_forall_exists_fun

deleted theorem mem_span_image_iff_exists_fun

deleted theorem mem_span_range_iff_exists_fun

deleted theorem mem_span_set'

deleted theorem mem_span_set

deleted theorem span_eq_iUnion_nat

deleted theorem top_le_span_range_iff_forall_exists_fun

Modified Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean

Modified Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean

Modified Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

added theorem Ideal.mem_span_range_iff_exists_fun

deleted theorem mem_ideal_span_range_iff_exists_fun

Modified Mathlib/RingTheory/Localization/Away/Basic.lean

Modified Mathlib/RingTheory/RingHom/Locally.lean

Modified Mathlib/Topology/Algebra/Module/Basic.lean