Commit 2023-12-30 03:42 f656e606

View on Github →

chore: Move misplaced lemmas in Mathlib/LinearAlgebra/FreeModule/Finite/Rank.lean. (#9301)

Estimated changes

Modified Mathlib/LinearAlgebra/FreeModule/Finite/Rank.lean

deleted theorem Module.Finite.span_of_finite

deleted theorem Submodule.fg_iff_finite

Modified Mathlib/RingTheory/Finiteness.lean

added theorem Module.Finite.iff_fg

added theorem Module.Finite.span_of_finite