Def ConvexCone.toPointedCone

Modification history

2025-08-21 11:59

Mathlib/Geometry/Convex/Cone/Pointed.lean

refactor: make the cone explicit in `ConvexCone.toPointedCone` (#28139) …

Modified ConvexCone.toPointedCone View on Github →

2025-06-19 10:04

Mathlib/Geometry/Convex/Cone/Pointed.lean

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

Modified ConvexCone.toPointedCone View on Github →

2023-09-29 03:32

Mathlib/Analysis/Convex/Cone/Pointed.lean

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

Added ConvexCone.toPointedCone View on Github →