Commit 2025-04-15 10:53 aa17f77c

chore(Finsupp/Interval): remove open scoped Classical (#24055) Removing it from the definitions is easier than adding it to all the theorems and adding converts as appropriate. This has a knock-on effect on MvPowerSeries, but "you must be able to tell which variable is which" is hardly demanding!