Commit 2023-11-10 18:21 b0bb59ce

View on Github →

feat: Minkowski Convex Body Theorem for compact convex body (#8274)

Estimated changes

Modified Mathlib/Analysis/Convex/Body.lean

added theorem ConvexBody.iInter_smul_eq_self

added theorem ConvexBody.smul_le_of_le

added theorem ConvexBody.zero_mem_of_symmetric

Modified Mathlib/MeasureTheory/Group/GeometryOfNumbers.lean

added theorem MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_le_measure

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean

Modified Mathlib/Topology/Separation.lean

added theorem isOpen_inter_eq_singleton_of_mem_discrete