Theorem exists_smul_eq_of_finrank_eq_one

Modification history

2024-07-15 10:14

Mathlib/LinearAlgebra/FiniteDimensional.lean

chore: split LinearAlgebra.FiniteDimensional (#14670) …

Modified exists_smul_eq_of_finrank_eq_one View on Github →

2023-08-19 18:38

Mathlib/LinearAlgebra/FiniteDimensional.lean

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

Added exists_smul_eq_of_finrank_eq_one View on Github →