Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-09 21:23 d7cebcf6

View on Github →

feat(linear_algebra/multilinear): basics of multilinear maps (#1814)

  • multilinear maps
  • progress
  • isomorphisms
  • Update src/logic/function.lean Co-Authored-By: Johan Commelin [email protected]
  • better docstring
  • variable module
  • dep cons
  • make everything dependent
  • remove print statement
  • fix build
  • Update src/linear_algebra/multilinear.lean Co-Authored-By: Chris Hughes [email protected]
  • Update src/linear_algebra/multilinear.lean Co-Authored-By: Chris Hughes [email protected]
  • fixes
  • docstrings
  • reviewer's comments
  • cleanup

Estimated changes

added theorem fin.cast_succ_ne_last
modified def fin.cons
added theorem fin.cons_self_tail
modified theorem fin.cons_succ
added theorem fin.cons_update
modified theorem fin.cons_zero
added theorem fin.injective_succ
added theorem fin.succ_inj
modified def fin.tail
modified theorem fin.tail_cons
added theorem fin.tail_update_succ
added theorem fin.tail_update_zero
added theorem fin.update_cons_zero
added def fin_zero_elim'
deleted def {u}
added theorem multilinear_map.ext
added structure multilinear_map
added theorem function.update_comp
modified theorem function.update_noteq
modified theorem function.update_same