Theorem Submodule.disjoint_span_singleton_of_not_mem

Modification history

2025-05-25 12:30

Mathlib/LinearAlgebra/Span/Basic.lean

chore(*): not_mem/nmem -> notMem (#25159)

Deleted Submodule.disjoint_span_singleton_of_not_mem View on Github →

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 →