Commit 2024-04-12 15:16 b0aea615

View on Github →

feat: Generalize corollaries of rank-nullity theorem. (#9626) Added a class HasRankNullity consisting of the rings that satisfy the rank-nullity theorem. Generalized the corollaries of the rank-nullity theorem from division rings to rings satisfying the class, and moved them into a new file LinearAlgebra.Dimension.RankNullity.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/Dimension/Constructions.lean

added theorem LinearIndependent.sum_elim_of_quotient

added theorem LinearIndependent.union_of_quotient

Modified Mathlib/LinearAlgebra/Dimension/DivisionRing.lean

deleted theorem Submodule.rank_add_le_rank_add_rank

deleted theorem Submodule.rank_sup_add_rank_inf_eq

deleted theorem exists_linearIndependent_cons_of_lt_finrank

deleted theorem exists_linearIndependent_cons_of_lt_rank

deleted theorem exists_linearIndependent_pair_of_one_lt_finrank

deleted theorem exists_linearIndependent_pair_of_one_lt_rank

deleted theorem exists_linearIndependent_snoc_of_lt_finrank

deleted theorem exists_linearIndependent_snoc_of_lt_rank

deleted theorem rank_eq_of_surjective

deleted theorem rank_quotient_add_rank

added theorem rank_quotient_add_rank_of_divisionRing

deleted theorem rank_range_add_rank_ker

Modified Mathlib/LinearAlgebra/Dimension/Finite.lean

added theorem exists_finset_linearIndependent_of_le_finrank

added theorem exists_finset_linearIndependent_of_le_rank

added theorem exists_linearIndependent_of_le_finrank

added theorem exists_linearIndependent_of_le_rank

added theorem exists_set_linearIndependent_of_lt_rank

added theorem natCast_le_rank_iff

added theorem natCast_le_rank_iff_finset

Modified Mathlib/LinearAlgebra/Dimension/Localization.lean

added theorem IsLocalizedModule.linearIndependent_lift

added theorem aleph0_le_rank_of_isEmpty_oreSet

added theorem exists_set_linearIndependent_of_isDomain

added theorem nonempty_oreSet_of_strongRankCondition

Created Mathlib/LinearAlgebra/Dimension/RankNullity.lean

added theorem Submodule.rank_add_le_rank_add_rank

added theorem Submodule.rank_sup_add_rank_inf_eq

added theorem exists_linearIndependent_cons_of_lt_finrank

added theorem exists_linearIndependent_cons_of_lt_rank

added theorem exists_linearIndependent_of_lt_rank

added theorem exists_linearIndependent_pair_of_one_lt_finrank

added theorem exists_linearIndependent_pair_of_one_lt_rank

added theorem exists_linearIndependent_snoc_of_lt_finrank

added theorem exists_linearIndependent_snoc_of_lt_rank

added theorem exists_set_linearIndependent

added theorem exists_smul_not_mem_of_rank_lt

added theorem lift_rank_eq_of_surjective

added theorem lift_rank_range_add_rank_ker

added theorem rank_eq_of_surjective

added theorem rank_quotient_add_rank

added theorem rank_range_add_rank_ker

Modified Mathlib/Logic/Embedding/Set.lean

Modified Mathlib/NumberTheory/Modular.lean

Modified Mathlib/RingTheory/OreLocalization/OreSet.lean

added theorem OreLocalization.nonempty_oreSet_iff

added theorem OreLocalization.nonempty_oreSet_iff_of_noZeroDivisors

Modified docs/references.bib