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)

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