Commit 2023-12-09 23:54 06295115

View on Github →

chore(Order/Filter): protect Filter.map_smul (#8935) We use SMulHomClass.map_smul much more often, even when the Filter namespace is opened.

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Free.lean

Modified Mathlib/Algebra/Module/Submodule/Bilinear.lean

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

Modified Mathlib/LinearAlgebra/Basis.lean

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

Modified Mathlib/Order/Filter/Pointwise.lean

deleted theorem Filter.map_smul

modified theorem Filter.mem_smul_filter

Modified Mathlib/Topology/Algebra/UniformConvergence.lean