mathlib
ebf73435 - feat(analysis/normed*): add instances and lemmas (#15515)

Commit

3 years ago

feat(analysis/normed*): add instances and lemmas (#15515) * Add some `coe_*` lemmas. * Add `is_scalar_tower` and `is_smul_class` instances.

Author

urkud

Parents