Theorem Submodule.disjoint_span_singleton_of_not_mem

Modification history

2025-01-03 05:55

Mathlib/LinearAlgebra/Span/Basic.lean

chore(LinearAlgebra/Span/Basic): move/add lemmas about span_singleton (#20397)

Added Submodule.disjoint_span_singleton_of_not_mem View on Github →