mathlib
9505e5b3
- fix(data/matrix): use pi.module for the module structure (#1242)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
6 years ago
fix(data/matrix): use pi.module for the module structure (#1242) * fix(data/matrix): use pi.module for the module structure * Update matrix.lean * Update matrix.lean * Update matrix.lean
References
#1242 - fix(data/matrix): use pi.module for the module structure
Author
ChrisHughes24
Committer
mergify[bot]
Parents
07ae80f4
Loading