mathlib
54773fc0
- feat(topology/algebra/module/multilinear): add `continuous_multilinear_map.smul_right` (#14218)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
feat(topology/algebra/module/multilinear): add `continuous_multilinear_map.smul_right` (#14218) See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Question.20about.20.60formal_multilinear_series.60 for one use case
Author
ADedecker
Parents
9dc9c3ea
Loading