Theorem Module.Basis.nonempty_unique_index_of_finrank_eq_one

Modification history

2025-11-16 15:54
Mathlib/LinearAlgebra/Dimension/Free.lean
feat(LinearAlgebra/SpecialLinearGroup): special linear group of a module (#30987) …
Added Module.Basis.nonempty_unique_index_of_finrank_eq_oneView on Github →