mathlib3
c78cad35
- chore(analysis/inner_product_space/basic): explicit `𝕜` argument for `innerₛₗ` and `innerSL` (#18613)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
2 years ago
chore(analysis/inner_product_space/basic): explicit `𝕜` argument for `innerₛₗ` and `innerSL` (#18613) A reasonable fraction of the uses of these functions required either `@` or a type annotation before this change.
Author
eric-wieser
Parents
1dac236e
Loading