mathlib3
d5d57849 - chore(ring_theory/power_basis): add `simps` (#11766)

Commit
4 years ago
chore(ring_theory/power_basis): add `simps` (#11766) for flt-regular
Author
Parents
Loading