Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-15 21:05 bc5d5c9d

View on Github →

feat(data/matrix/notation,data/fin): head and append simp (#5741)

Estimated changes

Modified src/data/fin.lean

added theorem fin.fin_append_apply_zero

Modified src/data/matrix/notation.lean

added theorem matrix.head_fin_const

added theorem matrix.vec_head_vec_alt0

added theorem matrix.vec_head_vec_alt1