mathlib
d0f45f52
- lint(various): nolint has_inhabited_instance for injective functions (#4541)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
lint(various): nolint has_inhabited_instance for injective functions (#4541) `function.embedding`, `homeomorph`, `isometric` represent injective/bijective functions, so it's silly to expect them to be inhabited.
References
#4925 - Make prime-avoidance branch build
Author
hrmacbeth
Parents
cc75e4ef
Loading