Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-31 20:07 26a62b0d

View on Github →

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

Estimated changes