Commit 2025-06-12 10:35 d041e192

View on Github →

refactor: redefine ProperCone as an abbrev for ClosedSubmodule (#25204) ... and derive the ProperCone operations from ClosedSubmodule too. Also rename the scalar ring from 𝕜 to R. From Toric

Estimated changes

added theorem ProperCone.coe_bot
modified theorem ProperCone.coe_comap
modified theorem ProperCone.coe_map
deleted theorem ProperCone.coe_positive
deleted theorem ProperCone.coe_zero
modified theorem ProperCone.comap_comap
modified theorem ProperCone.comap_id
modified theorem ProperCone.ext
modified theorem ProperCone.map_id
added theorem ProperCone.mem_bot
deleted theorem ProperCone.mem_coe
modified theorem ProperCone.mem_comap
modified theorem ProperCone.mem_map
modified theorem ProperCone.mem_positive
deleted theorem ProperCone.mem_zero
deleted theorem ProperCone.pointed_zero
modified def ProperCone.positive
deleted structure ProperCone