Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-28 09:40 105935c0

View on Github →

feat(linear_algebra/finite_dimensional): characterizations of finrank = 1 and ≤ 1 (#7354)

Estimated changes

Modified src/linear_algebra/affine_space/independent.lean

Modified src/linear_algebra/basic.lean

added theorem submodule.span_singleton_eq_top_iff

Modified src/linear_algebra/basis.lean

added theorem is_basis_singleton_iff

Modified src/linear_algebra/finite_dimensional.lean

added theorem finite_dimensional.exists_is_basis_singleton

modified theorem finite_dimensional.finrank_zero_of_subsingleton

added theorem finrank_eq_one

added theorem finrank_eq_one_iff'

added theorem finrank_eq_one_iff

added theorem finrank_eq_one_iff_of_nonzero

added theorem finrank_le_one

added theorem finrank_le_one_iff

added theorem singleton_is_basis

Modified src/linear_algebra/linear_independent.lean

modified theorem linear_independent_unique_iff