mathlib3
4b217ea7
- chore(topology/algebra): rename file to match renamed lemmas (#11996)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
chore(topology/algebra): rename file to match renamed lemmas (#11996) #11940 renamed the lemmas from `continuous_smulâ‚‚` to `continuous_const_smul`, so this renames the file from `mul_action2` to `const_mul_action` accordingly.
Author
eric-wieser
Parents
4a4a3a90
Loading