Commit 2026-07-29 18:35 077102ea

View on Github →

feat(LinearAlgebra/Dimension/Free): isomorphic to base ring iff rank is one (#37959)

Estimated changes

Modified Mathlib/LinearAlgebra/Dimension/Free.lean

added theorem Module.nonempty_algEquiv_iff_finrank_eq_one

added theorem Module.nonempty_linearEquiv_iff_finrank_eq_one

added theorem Module.nonempty_linearEquiv_iff_rank_eq_one

deleted theorem Module.nonempty_linearEquiv_of_finrank_eq_one