Commit 2024-10-20 12:53 d1729028

View on Github →

chore(Algebra/Order/BigOperators/Group/Finset): don't import Ring (#17939) By moving the positivity extension, one can shave off a bunch of imports

Estimated changes