Theorem Submodule.span_eq_closure

Modification history

2024-11-15 15:51

Mathlib/LinearAlgebra/Span/Basic.lean

chore(LinearAlgebra/Span): split off definition of `Submodule.span` (#18618) …

Modified Submodule.span_eq_closure View on Github →

2024-01-06 09:51

Mathlib/LinearAlgebra/Span.lean

feat: generalize `Module.Finite.trans` (#9380) …

Added Submodule.span_eq_closure View on Github →