Commit 2023-08-19 18:38 1a978e5c

View on Github →

feat(LinearAlgebra): complements on spaces of dimension >1 or >n (#6348)

Estimated changes

Modified Mathlib/LinearAlgebra/Dimension.lean

added theorem exists_linear_independent_cons_of_lt_rank

added theorem exists_linear_independent_pair_of_one_lt_rank

added theorem exists_linear_independent_snoc_of_lt_rank

Modified Mathlib/LinearAlgebra/FiniteDimensional.lean

added theorem exists_smul_eq_of_finrank_eq_one

Modified Mathlib/LinearAlgebra/Finrank.lean

added theorem FiniteDimensional.lt_rank_of_lt_finrank

added theorem FiniteDimensional.one_lt_rank_of_one_lt_finrank

deleted theorem FiniteDimensional.rank_lt_of_finrank_lt

added theorem exists_linear_independent_cons_of_lt_finrank

added theorem exists_linear_independent_pair_of_one_lt_finrank

added theorem exists_linear_independent_snoc_of_lt_finrank

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

added theorem LinearIndependent.eq_of_pair

added theorem LinearIndependent.eq_zero_of_pair