Commit 2025-05-29 03:47 a8f4f9af

View on Github →

chore(Geometry/Convex/Cone/Basic): rename variables (#25252) Replace 𝕜 by R when it's merely a ring, and E, F, G by M, N, O (since they aren't normed). From Toric

Estimated changes

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

modified def Convex.toCone

modified theorem Convex.toCone_eq_sInf

modified theorem Convex.toCone_isLeast

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 theorem ConvexCone.Pointed.mono

modified def ConvexCone.Pointed

modified theorem ConvexCone.Salient.anti

modified theorem ConvexCone.blunt_iff_not_pointed

modified theorem ConvexCone.blunt_strictlyPositive

modified theorem ConvexCone.coe_bot

modified theorem ConvexCone.coe_comap

modified theorem ConvexCone.coe_iInf

modified theorem ConvexCone.coe_inf

modified theorem ConvexCone.coe_map

modified theorem ConvexCone.coe_mk

modified theorem ConvexCone.coe_positive

modified theorem ConvexCone.coe_sInf

modified theorem ConvexCone.coe_strictlyPositive

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_bot

modified theorem ConvexCone.mem_comap

modified theorem ConvexCone.mem_iInf

modified theorem ConvexCone.mem_map

modified theorem ConvexCone.mem_mk

modified theorem ConvexCone.mem_positive

modified theorem ConvexCone.mem_sInf

modified theorem ConvexCone.mem_strictlyPositive

modified theorem ConvexCone.mem_top

modified theorem ConvexCone.mem_zero

modified theorem ConvexCone.pointed_iff_not_blunt

modified theorem ConvexCone.pointed_positive

modified theorem ConvexCone.pointed_zero

modified def ConvexCone.positive

modified theorem ConvexCone.positive_le_strictlyPositive

modified theorem ConvexCone.salient_iff_not_flat

modified theorem ConvexCone.salient_positive

modified theorem ConvexCone.salient_strictlyPositive

modified theorem ConvexCone.smul_mem

modified theorem ConvexCone.smul_mem_iff

modified def ConvexCone.strictlyPositive

modified def ConvexCone.toPartialOrder

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.pointed_toConvexCone

modified def Submodule.toConvexCone

modified theorem Submodule.toConvexCone_bot

modified theorem Submodule.toConvexCone_inf

modified theorem Submodule.toConvexCone_le_iff

modified theorem Submodule.toConvexCone_top

modified theorem convexHull_toCone_eq_sInf

modified theorem convexHull_toCone_isLeast