mathlib3
d8384ddf
- remove `@[simps]` of `adjoin_root.power_basis_aux'` and `adjoin_root.power_basis'`
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
2 years ago
remove `@[simps]` of `adjoin_root.power_basis_aux'` and `adjoin_root.power_basis'`
Author
astrainfinita
Parents
23fdac64
Loading