Def Submodule.ofLinearComb

Modification history

2025-10-27 15:31
Mathlib/Algebra/Module/Submodule/Defs.lean
feat: constructor for submodules and pointed cones from two-element closures (#27578) …
Added Submodule.ofLinearCombView on Github →