mathlib3
b7978f39
- chore(analysis/seminorm): Weaken typeclasses on `convex` and `locally_convex` lemmas (#12645)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
chore(analysis/seminorm): Weaken typeclasses on `convex` and `locally_convex` lemmas (#12645) Generalize type-classes `normed_linearly_ordered_field` to `normed_field` (otherwise it would not work over complex numbers).
Author
mcdoll
Parents
53f6d687
Loading