TotalPositiveCone

Stream: mathlib4

[Yury G. Kudryashov]

Do we need docs#AddCommGroup.PositiveCone, docs#AddCommGroup.TotalPositiveCone etc?

[Yury G. Kudryashov]

Added by @Mario Carneiro as a typeclass in 2017, converted to a structure by @Scott Morrison in 2021

[Yury G. Kudryashov]

#10868

[Mario Carneiro]

I did? I'm pretty sure this was originally just a smart constructor, and someone wanted it to be a structure to make the constructor easier to use

[Mario Carneiro]

I feel like the promotion to a structure has given this more legitimacy than it deserves

[Mario Carneiro]

it was only ever meant as a way to construct a partially or totally ordered group using a unary "is positive" predicate

[Yury G. Kudryashov]

https://github.com/leanprover-community/mathlib/commit/a1c3e2defc89c1bc792cb34caf9947dd77aabd3f

[Yury G. Kudryashov]

#10868 keeps failing on "get cache". Any ideas why?

[Mario Carneiro]

could be an import cycle?

[Mario Carneiro]

indeed Mathlib.Algebra.Order.Ring.Cone imports itself

[Yury G. Kudryashov]

:face_palm: