mathlib3
26a62b0d - fix(topology/algebra/module/multilinear): initialize simps projections (#14495)

Commit
3 years ago
fix(topology/algebra/module/multilinear): initialize simps projections (#14495) * `continuous_multilinear_map.smul_right` has a `simps` attribute, causing the generation of the simps projections for `continuous_multilinear_map`, but without specific support for apply. We now initialize the simps projections correctly. * This fixes an error in the sphere eversion project
Author
Parents
Loading