Theorem Submodule.neg_restrictScalars

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) …
Added Submodule.neg_restrictScalarsView on Github →