nonsingular_inverse): more lemmas (#8216)

Commit

4 years ago

feat(linear_algebra/matrix/nonsingular_inverse): more lemmas (#8216) add more defs and lemmas Co-authored-by: l534zhan <84618936+l534zhan@users.noreply.github.com>

Author

l534zhan

Parents

b52c1f0c

mathlib d0e09dde - feat(linear_algebra/matrix/nonsingular_inverse): more lemmas (#8216)

mathlib
d0e09dde - feat(linear_algebra/matrix/nonsingular_inverse): more lemmas (#8216)