Def PointedCone.positive

Modification history

2026-06-30 20:40

Mathlib/Geometry/Convex/Cone/Pointed.lean

refactor: change definitions to avoid `ConvexCone` (#37420) …

Modified PointedCone.positive View on Github →

2025-06-19 10:04

Mathlib/Geometry/Convex/Cone/Pointed.lean

chore(Geometry/Convex/Cone): clean up (#25291) …

Modified PointedCone.positive View on Github →

2023-09-29 03:32

Mathlib/Analysis/Convex/Cone/Pointed.lean

feat(Analysis): define pointed cones (#6437) …

Added PointedCone.positive View on Github →