mathlib3
43f1af99
- refactor(topology/continuous_function/basic): rename `map_specialization` (#14565)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
refactor(topology/continuous_function/basic): rename `map_specialization` (#14565) Rename `continuous_map.map_specialization` to `continuous_map.map_specializes` to align with the name of the relation.
Author
urkud
Parents
544fdc0d
Loading