Skip to content

Commit 22a8c45

Browse files
mcdollurkud
andcommitted
feat: port Analysis.Convex.Cone.Basic (#4152)
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
1 parent a4dbf4c commit 22a8c45

File tree

2 files changed

+861
-0
lines changed

2 files changed

+861
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -400,6 +400,7 @@ import Mathlib.Analysis.Convex.Body
400400
import Mathlib.Analysis.Convex.Caratheodory
401401
import Mathlib.Analysis.Convex.Combination
402402
import Mathlib.Analysis.Convex.Complex
403+
import Mathlib.Analysis.Convex.Cone.Basic
403404
import Mathlib.Analysis.Convex.Contractible
404405
import Mathlib.Analysis.Convex.Exposed
405406
import Mathlib.Analysis.Convex.Extrema

0 commit comments

Comments
 (0)