Commit 2024-06-13 08:41 a6db0214

View on Github →

chore: split Mathlib.Topology.Algebra.UniformConvergence (#13738) This reduces the longest pole by two files.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

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

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

Created Mathlib/Topology/Algebra/Module/UniformConvergence.lean

added theorem UniformFun.continuousSMul_induced_of_range_bounded

added theorem UniformOnFun.continuousSMul_induced_of_image_bounded

added theorem UniformOnFun.continuousSMul_submodule_of_image_bounded

Modified Mathlib/Topology/Algebra/UniformConvergence.lean

deleted theorem UniformFun.continuousSMul_induced_of_range_bounded

deleted theorem UniformOnFun.continuousSMul_induced_of_image_bounded

deleted theorem UniformOnFun.continuousSMul_submodule_of_image_bounded