feat(data/matrix/basic): miscellaneous defs and lemmas (#8289)
miscellaneous defs and lemmas
Co-authored-by: l534zhan <luming.zhang@merton.ox.ac.uk>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: l534zhan <84618936+l534zhan@users.noreply.github.com>
