Commit 2025-10-11 05:45 c4b0fc93

View on Github →

feat: a PointedCone-valued version of Submodule.span (#28140) This is merely to guide typing. From Toric

Estimated changes

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

modified theorem PointedCone.dual_span

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

modified theorem PointedCone.mem_toConvexCone

added theorem PointedCone.subset_span