Commit 2023-02-13 06:32 c0bcf2cb

View on Github →

feat: port Topology.Algebra.MulAction (#2013)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/MulAction.lean

added theorem Continuous.smul

added theorem ContinuousAt.smul

added theorem ContinuousOn.smul

added theorem ContinuousWithinAt.smul

added theorem Filter.Tendsto.smul

added theorem Filter.Tendsto.smul_const

added theorem continuousSMul_inf

added theorem continuousSMul_infᵢ

added theorem continuousSMul_infₛ