reflection): lemmas for arbitrary concrete matrices, proved via reflection (#18711)

Commit

2 years ago

feat(data/matrix/reflection): lemmas for arbitrary concrete matrices, proved via reflection (#18711) Split from #15738. This contains no meta code, so should be straightforward to port to mathlib4.

Author

eric-wieser

Parents

e5820f6c

mathlib3 d95bef0d - feat(data/matrix/reflection): lemmas for arbitrary concrete matrices, proved via reflection (#18711)

mathlib3
d95bef0d - feat(data/matrix/reflection): lemmas for arbitrary concrete matrices, proved via reflection (#18711)