Commit 2025-01-03 05:55 add4d4ae

View on Github →

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

Estimated changes

Modified Mathlib/LinearAlgebra/Span/Basic.lean

modified theorem Submodule.covBy_span_singleton_sup

modified theorem Submodule.disjoint_span_singleton'

modified theorem Submodule.disjoint_span_singleton

added theorem Submodule.disjoint_span_singleton_of_not_mem

added theorem Submodule.isCompl_span_singleton_of_isCoatom_of_not_mem

modified theorem Submodule.wcovBy_span_singleton_sup