Commit 2026-04-03 13:06 0dd5d5f5

View on Github →

chore(Geometry/Convex/Cone): deprecate ConvexCone.IsGenerating (#37417) This definition is not being used even in PRs where it would be natural to (eg #34848), so it should be removed

Estimated changes

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

deleted theorem ConvexCone.IsGenerating.isReproducing

modified def ConvexCone.IsGenerating

deleted theorem ConvexCone.IsReproducing.isGenerating

added theorem ConvexCone.IsReproducing.of_span_eq_top

added theorem ConvexCone.IsReproducing.span_eq_top

deleted theorem ConvexCone.isGenerating_iff_isReproducing

added theorem ConvexCone.span_eq_top_iff_isReproducing