Commit 2026-06-30 20:40 4bf1ddae
View on Github →refactor: change definitions to avoid ConvexCone (#37420)
Change the definitions of PointedCone.positive and PointedCone.closure to avoid mentioning ConvexCone.
This PR is part of a series deprecating ConvexCone: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Replacing.20.60ConvexCone.60.20with.20.60PointedCone.60/with/582738985