mathlib
e6f8ad79 - refactor(analysis/convex/cone): generalize ℝ to an ordered semiring (#9481)

Commit
4 years ago
refactor(analysis/convex/cone): generalize ℝ to an ordered semiring (#9481) Currently, `convex_cone` is only defined in ℝ-modules. This generalizes ℝ to an arbitray ordered semiring. `convex_cone E` is now spelt `convex_cone 𝕜 E`. Similarly, `positive_cone E` becomes `positive_cone 𝕜 E`.
Author
Parents
Loading