Commit 2023-08-03 09:17 421f759a

View on Github →

chore: remove duplicate lemma FiniteDimensional.eq_top_of_finrank_eq (#6304) The lemma is a perfect duplicate of Submodule.eq_top_of_finrank_eq.

Estimated changes

Modified Mathlib/FieldTheory/Tower.lean

Modified Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean

Modified Mathlib/LinearAlgebra/BilinearForm.lean

Modified Mathlib/LinearAlgebra/Dual.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional.lean

deleted theorem FiniteDimensional.eq_top_of_finrank_eq

modified theorem Submodule.eq_top_of_finrank_eq

Modified Mathlib/Topology/Algebra/Module/FiniteDimension.lean