mathlib
21e3562c
- chore(data/matrix/basic): add a star_module instance (#18557)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
2 years ago
chore(data/matrix/basic): add a star_module instance (#18557) We already have instances for the other star properties, but missed this one.
Author
eric-wieser
Parents
d23150d1
Loading