Commit 2023-12-18 12:58 302fdbb8

View on Github →

chore: Generalize results on finrank to rings. (#8912) A portion of results in Mathlib/LinearAlgebra/FiniteDimensional.lean were generalized to rings and moved to Mathlib/LinearAlgebra/FreeModule/Finite/Rank.lean. Most API lemmas for FiniteDimensional are kept but replaced with one lemma proofs. Definitions and niche lemmas are replaced by the generalized version completely.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

Modified Mathlib/Analysis/InnerProductSpace/l2Space.lean

Modified Mathlib/LinearAlgebra/Dimension.lean

added theorem rank_eq_zero_iff

added theorem rank_eq_zero_iff_isTorsion

added theorem rank_span_finset_le

added theorem rank_span_le_of_finite

modified theorem rank_span_of_finset

Modified Mathlib/LinearAlgebra/Dual.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional.lean

deleted theorem CompleteLattice.Independent.subtype_ne_bot_le_finrank

deleted theorem CompleteLattice.Independent.subtype_ne_bot_le_finrank_aux

deleted theorem FiniteDimensional.basisUnique.repr_eq_zero_iff

deleted theorem FiniteDimensional.cardinal_mk_le_finrank_of_linearIndependent

deleted theorem FiniteDimensional.exists_nontrivial_relation_of_rank_lt_card

deleted theorem FiniteDimensional.exists_nontrivial_relation_sum_zero_of_rank_succ_lt_card

added theorem FiniteDimensional.exists_relation_sum_zero_pos_coefficient_of_finrank_succ_lt_card

deleted theorem FiniteDimensional.exists_relation_sum_zero_pos_coefficient_of_rank_succ_lt_card

modified theorem FiniteDimensional.fact_finiteDimensional_of_finrank_eq_succ

modified theorem FiniteDimensional.finiteDimensional_of_finrank

deleted theorem FiniteDimensional.finrank_pos

deleted theorem FiniteDimensional.finrank_pos_iff

deleted theorem FiniteDimensional.finrank_pos_iff_exists_ne_zero

deleted theorem FiniteDimensional.finrank_zero_iff

deleted theorem FiniteDimensional.finset_card_le_finrank_of_linearIndependent

deleted theorem FiniteDimensional.fintype_card_le_finrank_of_linearIndependent

deleted theorem FiniteDimensional.not_linearIndependent_of_infinite

modified theorem FiniteDimensional.of_fintype_basis

deleted theorem LinearIndependent.finite

deleted theorem LinearIndependent.setFinite

deleted theorem bot_eq_top_of_rank_eq_zero

deleted theorem finrank_eq_zero

deleted theorem finrank_eq_zero_of_rank_eq_zero

deleted theorem rank_eq_zero

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

modified theorem Module.Finite.of_basis

added theorem Module.Free.finite_basis

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

added theorem CompleteLattice.Independent.subtype_ne_bot_le_finrank

added theorem CompleteLattice.Independent.subtype_ne_bot_le_finrank_aux

added theorem FiniteDimensional.basisUnique_repr_eq_zero_iff

added theorem FiniteDimensional.cardinal_mk_le_finrank_of_linearIndependent

added theorem FiniteDimensional.finrank_eq_zero_iff

added theorem FiniteDimensional.finrank_eq_zero_iff_isTorsion

added theorem FiniteDimensional.finrank_eq_zero_of_rank_eq_zero

modified theorem FiniteDimensional.finrank_finsupp

added theorem FiniteDimensional.finrank_finsupp_self

added theorem FiniteDimensional.finrank_of_not_finite

added theorem FiniteDimensional.finrank_pos

added theorem FiniteDimensional.finrank_pos_iff

added theorem FiniteDimensional.finrank_pos_iff_exists_ne_zero

added theorem FiniteDimensional.finrank_zero_iff

added theorem FiniteDimensional.finset_card_le_finrank_of_linearIndependent

added theorem FiniteDimensional.fintype_card_le_finrank_of_linearIndependent

added theorem LinearIndependent.finite

added theorem LinearIndependent.setFinite

added theorem Module.Finite.lt_aleph0_of_linearIndependent

added theorem Module.Finite.not_linearIndependent_of_infinite

added theorem Module.Finite.span_of_finite

added theorem Module.exists_nontrivial_relation_of_finrank_lt_card

added theorem Module.exists_nontrivial_relation_sum_zero_of_finrank_succ_lt_card

added theorem Module.finite_iff_of_rank_eq_nsmul

added theorem Module.finite_of_finrank_eq_succ

added theorem Module.finite_of_finrank_pos

added theorem Module.finite_of_rank_eq_nat

added theorem Module.finite_of_rank_eq_one

added theorem Module.finite_of_rank_eq_zero

added theorem Module.mk_finrank_eq_card_basis

added theorem Module.rank_lt_alpeh0_iff

added theorem Submodule.bot_eq_top_of_rank_eq_zero

added theorem Submodule.fg_iff_finite

added theorem Submodule.finrank_eq_zero

added theorem Submodule.rank_eq_zero

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

Modified Mathlib/RingTheory/Finiteness.lean

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

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