mathlib3
404a9125 - chore(ring_theory/adjoin/power_basis): add `simps` (#11018)

Commit
4 years ago
chore(ring_theory/adjoin/power_basis): add `simps` (#11018) Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>
Author
Parents
Loading