Theorem LinearIndependent.span_eq_top_of_card_eq_finrank'

Modification history

2026-04-27 13:42

Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean

feat(LinearAlgebra/Basis/Fin): linear independence of `Fin.snoc` (#37810) …

Modified LinearIndependent.span_eq_top_of_card_eq_finrank'View on Github →

2024-02-15 06:24

Mathlib/LinearAlgebra/FiniteDimensional.lean

chore(LinearAlgebra): golf (#10569) …

Added LinearIndependent.span_eq_top_of_card_eq_finrank'View on Github →