Commit 2024-12-09 12:57 fc349f0c

View on Github →

chore: don't need group-theoretic exponent to set up finite dimensional vector spaces (#19827)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/FreeLocus.lean

Modified Mathlib/Algebra/Polynomial/Module/FiniteDimensional.lean

Modified Mathlib/Analysis/InnerProductSpace/Rayleigh.lean

Modified Mathlib/FieldTheory/Adjoin.lean

Modified Mathlib/FieldTheory/Finite/Polynomial.lean

Modified Mathlib/FieldTheory/SplittingField/Construction.lean

Modified Mathlib/LinearAlgebra/Dimension/DivisionRing.lean

deleted theorem lift_rank_lt_rank_dual'

deleted theorem lift_rank_lt_rank_dual

deleted theorem max_aleph0_card_le_rank_fun_nat

deleted theorem rank_dual_eq_card_dual_of_aleph0_le_rank'

deleted theorem rank_dual_eq_card_dual_of_aleph0_le_rank

deleted theorem rank_fun_infinite

deleted theorem rank_lt_rank_dual'

deleted theorem rank_lt_rank_dual

Created Mathlib/LinearAlgebra/Dimension/ErdosKaplansky.lean

added theorem lift_rank_lt_rank_dual'

added theorem lift_rank_lt_rank_dual

added theorem max_aleph0_card_le_rank_fun_nat

added theorem rank_dual_eq_card_dual_of_aleph0_le_rank'

added theorem rank_dual_eq_card_dual_of_aleph0_le_rank

added theorem rank_fun_infinite

added theorem rank_lt_rank_dual'

added theorem rank_lt_rank_dual

Modified Mathlib/LinearAlgebra/Dimension/Finite.lean

deleted theorem Module.finrank_eq_zero_iff_isTorsion

deleted theorem rank_eq_zero_iff_isTorsion

Renamed Mathlib/LinearAlgebra/Dimension/Torsion.lean to Mathlib/LinearAlgebra/Dimension/Torsion/Basic.lean

Created Mathlib/LinearAlgebra/Dimension/Torsion/Finite.lean

added theorem Module.finrank_eq_zero_iff_isTorsion

added theorem rank_eq_zero_iff_isTorsion

Modified Mathlib/LinearAlgebra/Dual.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional.lean

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

Modified Mathlib/LinearAlgebra/FreeModule/Norm.lean

Modified Mathlib/LinearAlgebra/Matrix/Diagonal.lean

Modified Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

Modified Mathlib/LinearAlgebra/Reflection.lean

Modified Mathlib/LinearAlgebra/Semisimple.lean

Modified Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral.lean

Modified Mathlib/NumberTheory/NumberField/Units/Basic.lean

Modified Mathlib/RepresentationTheory/Basic.lean

Modified Mathlib/RingTheory/Artinian.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

Modified Mathlib/RingTheory/LocalRing/Module.lean

Modified Mathlib/RingTheory/Polynomial/GaussLemma.lean

Modified Mathlib/RingTheory/PowerBasis.lean