mathlib3

12afc981 - chore(data/matrix/basic): instances for unique, subsing, nontriv, coe (#6296)

chore(data/matrix/basic): instances for unique, subsing, nontriv, coe (#6296) This adds a coercion to the underlying scalar if the matrix is 1 x 1. Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>