Def PointedCone.ofConeComb

Modification history

2025-10-27 15:31
Mathlib/Geometry/Convex/Cone/Pointed.lean
feat: constructor for submodules and pointed cones from two-element closures (#27578) …
Added PointedCone.ofConeCombView on Github →