Theorem Submodule.span_set_smul

Modification history

2026-04-15 08:14

Mathlib/Algebra/Module/Submodule/Pointwise.lean

chore(LinearAlgebra/Span): reverse import order between Submodule/Pointwise and Span/Basic (#38013) …

Modified Submodule.span_set_smul View on Github →

2024-05-22 06:25

Mathlib/Algebra/Module/Submodule/Pointwise.lean

Feat(Algebra/Module/Submodule/Pointwise): Generalize `set_smul_eq_iSup` as in TODO (#13103) …

Added Submodule.span_set_smul View on Github →