Commit 2025-11-14 14:18 f230ebbd

View on Github →

chore: rename FiniteDimensional.of_fintype_basis (#31543) The lemma has a Finite hypothesis now, not a Fintype one. The new name was discussed on zulip: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Naming.20convention/near/555088215

Estimated changes

Modified Archive/Sensitivity.lean

Modified Mathlib/Algebra/Module/ZLattice/Basic.lean

Modified Mathlib/Analysis/Normed/Module/FiniteDimension.lean

Modified Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean

Modified Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Properties.lean

Modified Mathlib/LinearAlgebra/Complex/FiniteDimensional.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean

deleted theorem FiniteDimensional.of_fintype_basis

added theorem Module.Basis.finiteDimensional_of_finite

Modified Mathlib/LinearAlgebra/PerfectPairing/Restrict.lean

Modified Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

Modified Mathlib/NumberTheory/FunctionField.lean

Modified Mathlib/RingTheory/Norm/Basic.lean

Modified Mathlib/RingTheory/Trace/Basic.lean

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