Commit 2026-03-21 06:41 e930a40e

View on Github →

feat(Geometry/Convex/Cone): lineality space of pointed cones (#33780) Define the lineality space PointedCone.lineal as the submodule C ⊓ -C. Prove that it is the largest submodule of the cone, which is sometimes used as an alternative definition.

Estimated changes

Modified Mathlib/Geometry/Convex/Cone/Pointed.lean

added theorem PointedCone.gc_ofSubmodule_lineal

added def PointedCone.lineal

added theorem PointedCone.lineal_eq_sSup

added theorem PointedCone.lineal_le

added theorem PointedCone.mem_lineal

added theorem PointedCone.ofSubmodule_lineal

added theorem PointedCone.support_eq