Commit 2025-10-27 15:31 4b887925
View on Github →feat: constructor for submodules and pointed cones from two-element closures (#27578) in Algebra/Module/Submodule/Defs.lean
- Construct a submodule from closure under two-element linear combinations. in Geometry/Convex/Cone/Pointed.lean
- Construct a pointed cone from closure under two-element conical combinations.
- lemma mem_span_set