Commit 2026-04-15 08:14 779f28ba

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

• Revert import order between Span/Basic and Submodule/Pointwise
• Remove import Submodule/Pointwise throughout mathlib because already imported via Span/Basic
• Move lemmas from Submodule/Pointwise to Span/Basic when they require the Span/Basic-import (except for span_neg_eq_neg which was moved for a different reason, see below).
• Rewriting part of Span/Basic to use pointwise notation (this was previously done for sets, and now it can be done for submodules as well). Adjust proofs to this change.
• use moved span_neg_eq_neg to shorten proof of span_neg. This is a follow up on #36689 in which is was noted that the import order might be the wrong way around.