Commit 2022-08-10 15:00 ac0996dd
View on Github →chore(topology/algebra/uniform_mul_action): the action of a ring on itself is uniformly continuous (#15974)
This proof can be used to golf the misnamed real.uniform_continuous_mul_const which is now called real.uniform_continuous_const_mul.