mathlib
0a3d1440
- chore(topology/algebra/uniform_mul_action): add `has_uniform_continuous_const_smul.op` (#12434)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
chore(topology/algebra/uniform_mul_action): add `has_uniform_continuous_const_smul.op` (#12434) This matches `has_continuous_const_smul.op` and other similar lemmas. With this in place, we can state `is_central_scalar` on `completion`s.
Author
eric-wieser
Parents
cac9242e
Loading