mathlib
26082445
- feat(data/matrix/basic): add lemma minor_map (#8074)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
feat(data/matrix/basic): add lemma minor_map (#8074) Add lemma `minor_map` proving that the operations of taking a minor and applying a map to the coefficients of a matrix commute.
Author
faenuccio
Parents
e137523a
Loading