Def ConvexCone.IsGenerating

Modification history

2026-04-03 13:06

Mathlib/Geometry/Convex/Cone/Basic.lean

chore(Geometry/Convex/Cone): deprecate `ConvexCone.IsGenerating` (#37417) …

Modified ConvexCone.IsGenerating View on Github →

2025-12-16 13:45

Mathlib/Geometry/Convex/Cone/Basic.lean

feat(Geometry/Convex/Cone): define and characterize generating convex cone (#32300) …

Added ConvexCone.IsGenerating View on Github →