Commit 2026-07-01 12:03 bb27e214

View on Github →

chore(LinearAlgebra/Dimension/Free): naming consistency (#41211)

Renames from discussion at https://github.com/leanprover-community/mathlib4/pull/37959/#discussion_r3142239137

Estimated changes

Modified Mathlib/LinearAlgebra/Basis/MulOpposite.lean

Modified Mathlib/LinearAlgebra/Complex/FiniteDimensional.lean

Modified Mathlib/LinearAlgebra/Dimension/Free.lean

deleted theorem LinearEquiv.nonempty_equiv_iff_lift_rank_eq

deleted theorem LinearEquiv.nonempty_equiv_iff_rank_eq

added theorem Module.nonempty_linearEquiv_iff_lift_rank_eq

added theorem Module.nonempty_linearEquiv_iff_rank_eq

Modified Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean