Commit 2026-03-05 13:43 998cee50

View on Github →

feat: two lemmas about ContinuousMultilinearMap (#36188)

  • Rename continuousMultilinearCurryFin0_symm_apply and remove its simp-lemma (simp can now prove it using the new simp-lemma)
  • Add a new version of continuousMultilinearCurryFin0_symm_apply.
  • The new lemma is very similar to the old one, and these lemmas are most likely to be used only by simp, so I don't think a deprecation cycle is needed.
  • Also add ContinuousMultilinearMap.fin0_apply_enorm Used for Sobolev spaces.

Estimated changes