Commit 2024-10-17 15:04 1cfdb12a

View on Github →

feat: Over a finite ring, a module is finite iff it is finite dimensional (#17707) From PFR

Estimated changes

Modified Mathlib/FieldTheory/AxGrothendieck.lean

Modified Mathlib/FieldTheory/PrimitiveElement.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean

deleted theorem FiniteDimensional.finite_of_finite

Modified Mathlib/RingTheory/Finiteness.lean

added theorem Module.finite_iff_finite

added theorem Module.finite_of_finite

added theorem Set.Finite.submoduleSpan

Modified Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean