Commit 2026-05-25 19:08 91e0d5b6

View on Github →

feat(Geometry/Convex/Cone): Minor additions to pointed cones (#37464) Minor additions to pointed cones:

  • PointedCone.ofSubmodule_le_ofSubmodule and PointedCone.ofSubmodule_lt_ofSubmodule. These are not made simp lemmas, instead the underlying Submodule.restrictScalars_le and Submodule.restrictScalars_lt have been changed into simp lemmas.
  • PointedCone.hull_le_span as a short form of Submodule.span_le_restrictScalars R≥0 R s Co-authored by: Artie Khovanov

Estimated changes

modified theorem PointedCone.mem_lineal
modified theorem PointedCone.neg_ofSubmodule
modified theorem PointedCone.support_eq