Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-01 20:36 e6f8ad79

View on Github →

refactor(analysis/convex/cone): generalize ℝ to an ordered semiring (#9481) Currently, convex_cone is only defined in ℝ-modules. This generalizes ℝ to an arbitray ordered semiring. convex_cone E is now spelt convex_cone 𝕜 E. Similarly, positive_cone E becomes positive_cone 𝕜 E.

Estimated changes

modified theorem convex.mem_to_cone'
modified theorem convex.mem_to_cone
modified def convex.to_cone
modified theorem convex.to_cone_eq_Inf
modified theorem convex.to_cone_is_least
modified def convex_cone.blunt
modified theorem convex_cone.coe_inf
modified def convex_cone.comap
modified theorem convex_cone.comap_comap
modified theorem convex_cone.comap_id
deleted theorem convex_cone.convex
modified theorem convex_cone.ext'
modified theorem convex_cone.ext
modified def convex_cone.flat
modified def convex_cone.map
modified theorem convex_cone.map_id
modified theorem convex_cone.map_map
modified theorem convex_cone.mem_Inf
modified theorem convex_cone.mem_bot
modified theorem convex_cone.mem_comap
modified theorem convex_cone.mem_mk
modified theorem convex_cone.mem_top
modified def convex_cone.pointed
modified def convex_cone.salient
modified theorem convex_cone.smul_mem
modified theorem convex_cone.smul_mem_iff
modified theorem convex_cone.to_ordered_smul
modified structure convex_cone
modified theorem riesz_extension