Commit 2026-03-13 09:45 e8fb0804

View on Github →

feat(Geometry/Convex/Cone): coercion from submodule to cone (#35308) Add coercion from submodule to cone and support lemmas. The main feature is

PointedCone.ofSubmodule coercing a submodule to a pointed cone and the corresponding Coe instance. There are further lemmas coercing membership and lattice operations.

Estimated changes

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

added theorem PointedCone.coe_ofSubmodule

added theorem PointedCone.mem_ofSubmodule_iff

added theorem PointedCone.ofSubmodule_iInf

added theorem PointedCone.ofSubmodule_iSup

added theorem PointedCone.ofSubmodule_inf

added theorem PointedCone.ofSubmodule_inj

added theorem PointedCone.ofSubmodule_sInf

added theorem PointedCone.ofSubmodule_sSup

added theorem PointedCone.ofSubmodule_sup