Commit 2025-04-06 17:49 7cf14df5

View on Github →

feat(RingTheory): length = dim for vector spaces (#23682)

Estimated changes

Modified Mathlib/LinearAlgebra/Dimension/Finite.lean

added theorem rank_pos_of_free

Modified Mathlib/RingTheory/Length.lean

modified theorem Module.length_bot

added theorem Module.length_eq_finrank

added theorem Module.length_eq_one

added theorem Module.length_eq_one_iff

added theorem Module.length_eq_rank

added theorem Module.length_eq_zero_of_subsingleton_ring

added theorem Module.length_finsupp

added theorem Module.length_of_free

added theorem Module.length_of_free_of_finite

added theorem Module.length_pi

added theorem Module.length_pi_of_fintype

added theorem Module.length_prod