Theorem Module.nonempty_algEquiv_iff_finrank_eq_one

Modification history

2026-07-29 18:35
Mathlib/LinearAlgebra/Dimension/Free.lean
feat(LinearAlgebra/Dimension/Free): isomorphic to base ring iff rank is one (#37959)
Added Module.nonempty_algEquiv_iff_finrank_eq_oneView on Github →