Theorem PointedCone.ofSubmodule_sInf

Modification history

2026-03-13 09:45
Mathlib/Geometry/Convex/Cone/Pointed.lean
feat(Geometry/Convex/Cone): coercion from submodule to cone (#35308) …
Added PointedCone.ofSubmodule_sInfView on Github →