Commit 2022-12-22 21:16 e172f2ae
View on Github →chore: clean up positivity stub theory (#1100)
Restore the lemmas for the so-far-implemented positivity extensions to their mathlib3 positions, attributes (they were all private), and typeclasses. Also remove nonsense instances of some typeclasses in the test file.
This things are all newly possible now that the underlying theory has been implemented.