Theorem PointedCone.neg_ofSubmodule

Modification history

2026-05-25 19:08
Mathlib/Geometry/Convex/Cone/Pointed.lean
feat(Geometry/Convex/Cone): Minor additions to pointed cones (#37464) …
Modified PointedCone.neg_ofSubmoduleView on Github →
2026-04-15 08:14
Mathlib/Geometry/Convex/Cone/Pointed.lean
chore(LinearAlgebra/Span): reverse import order between Submodule/Pointwise and Span/Basic (#38013) …
Added PointedCone.neg_ofSubmoduleView on Github →