Theorem Submodule.isCompl_span_singleton_of_isCoatom_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.isCompl_span_singleton_of_isCoatom_of_not_memView on Github →