Theorem Submodule.disjoint_span_singleton'

Modification history

2025-01-03 05:55

Mathlib/LinearAlgebra/Span/Basic.lean

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

Modified Submodule.disjoint_span_singleton'View on Github →

2023-08-10 19:52

Mathlib/LinearAlgebra/Span.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified Submodule.disjoint_span_singleton'View on Github →

2023-02-14 14:29

Mathlib/LinearAlgebra/Span.lean

feat: port LinearAlgebra.Span (#2248)

Added Submodule.disjoint_span_singleton'View on Github →