Commit 2023-03-02 09:07 8d0c08bd

View on Github →

feat: port Topology.Algebra.UniformMulAction (#2499)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/UniformMulAction.lean

added theorem UniformContinuous.const_smul

added theorem UniformSpace.Completion.coe_smul

added theorem UniformSpace.Completion.smul_def

added theorem uniformContinuousConstSMul_of_continuousConstSMul