LeanPool.VirasoroProject.ToMathlib.Topology.Algebra.ConstMulAction

theorem continuousConstSMul_of_discreteTopology (𝕜 : Type u_1) (X : Type u_2) [TopologicalSpace X] [DiscreteTopology X] [SMul 𝕜 X] : ContinuousConstSMul 𝕜 X