mathlib
ac0996dd - chore(topology/algebra/uniform_mul_action): the action of a ring on itself is uniformly continuous (#15974)

Commit
3 years ago
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`. Co-authored-by: Maria Ines de Frutos Fernandez <mariaines.dff@gmail.com>
Author
Parents
Loading