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
chore(Algebra/Order/BigOperators/Group/Finset): don't import Ring
(#17939)
By moving the positivity extension, one can shave off a bunch of imports