Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-03 11:26 62646673

View on Github →

refactor(linear_algebra/multilinear): cleanup of multilinear maps (#1921)

  • staging [ci skip]
  • staging
  • staging
  • cleanup norms
  • complete currying
  • docstrings
  • docstrings
  • cleanup
  • nonterminal simp
  • golf
  • missing bits for derivatives
  • sub_apply
  • cleanup
  • better docstrings
  • remove two files
  • reviewer's comments
  • use fintype
  • line too long

Estimated changes