mathlib
1e89df22
- chore(algebra/monoid_algebra): convert a filename prefix into a folder (#8925)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
chore(algebra/monoid_algebra): convert a filename prefix into a folder (#8925) This moves: * `algebra.monoid_algebra` to `algebra.monoid_algebra.basic` * `algebra.monoid_algebra_to_direct_sum` to `algebra.monoid_algebra.to_direct_sum`
Author
eric-wieser
Parents
98466d29
Loading