Commit 2025-06-19 10:04 34b7f046

View on Github →

chore(Geometry/Convex/Cone): clean up (#25291) Rename all the ConvexCones in the files to C, C₁, C₂. Previously they were S, T, K, K₁, K₂. Make sure to tag all the relevant lemmas with norm_cast. Fix lemma names. Golf proofs. From Toric

Estimated changes

modified theorem ConvexCone.Blunt.anti
modified theorem ConvexCone.Blunt.salient
modified def ConvexCone.Blunt
modified theorem ConvexCone.Flat.mono
modified theorem ConvexCone.Flat.pointed
modified def ConvexCone.Flat
modified theorem ConvexCone.Pointed.mono
modified def ConvexCone.Pointed
modified theorem ConvexCone.Salient.anti
modified def ConvexCone.Salient
deleted theorem ConvexCone.add_mem
added theorem ConvexCone.coe_add
modified theorem ConvexCone.coe_bot
modified theorem ConvexCone.coe_comap
modified theorem ConvexCone.coe_inf
modified theorem ConvexCone.coe_map
modified theorem ConvexCone.coe_mk
modified theorem ConvexCone.coe_sInf
modified theorem ConvexCone.coe_top
modified theorem ConvexCone.coe_zero
modified def ConvexCone.comap
modified theorem ConvexCone.comap_comap
modified theorem ConvexCone.comap_id
modified theorem ConvexCone.ext
modified def ConvexCone.map
modified theorem ConvexCone.map_id
modified theorem ConvexCone.map_map
modified theorem ConvexCone.mem_add
modified theorem ConvexCone.mem_comap
modified theorem ConvexCone.mem_iInf
modified theorem ConvexCone.mem_inf
modified theorem ConvexCone.mem_map
modified theorem ConvexCone.mem_mk
modified theorem ConvexCone.mem_positive
modified theorem ConvexCone.mem_sInf
modified theorem ConvexCone.mem_top
modified theorem ConvexCone.mem_zero
added theorem ConvexCone.notMem_bot
modified theorem ConvexCone.salient_positive
deleted theorem ConvexCone.smul_mem
modified theorem ConvexCone.smul_mem_iff
modified def ConvexCone.toPreorder
modified theorem ConvexCone.to_orderedSMul
modified structure ConvexCone
modified theorem Submodule.coe_toConvexCone
modified theorem Submodule.mem_toConvexCone
modified theorem Submodule.toConvexCone_bot
modified theorem Submodule.toConvexCone_inf
modified theorem Submodule.toConvexCone_top
modified theorem PointedCone.coe_comap
modified theorem PointedCone.coe_map
modified def PointedCone.comap
modified theorem PointedCone.comap_comap
modified theorem PointedCone.comap_id
added theorem PointedCone.convex
modified theorem PointedCone.ext
modified def PointedCone.map
modified theorem PointedCone.map_id
modified theorem PointedCone.map_map
modified theorem PointedCone.mem_comap
modified theorem PointedCone.mem_map
modified theorem PointedCone.mem_positive
modified def PointedCone.positive