Commit 2024-01-08 18:09 cabd20e0

View on Github →

feat: Rank-nullity theorem for commutative domains (#9412)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/LocalizedModule.lean

added theorem IsLocalizedModule.mk'_smul_mk'

Created Mathlib/Algebra/Module/Submodule/Localization.lean

added def Submodule.localized'

added def Submodule.toLocalized'

added def Submodule.toLocalizedQuotient'

added theorem Submodule.toLocalizedQuotient'_mk

Modified Mathlib/Algebra/Module/Zlattice.lean

Modified Mathlib/LinearAlgebra/Dimension/Constructions.lean

added theorem finrank_range_le_card

added theorem finrank_span_eq_card

added theorem finrank_span_finset_eq_card

added theorem finrank_span_finset_le_card

added theorem finrank_span_le_card

added theorem finrank_span_set_eq_card

added theorem rank_span_le

deleted theorem rank_span_le_of_finite

added theorem span_lt_of_subset_of_card_lt_finrank

added theorem span_lt_top_of_card_lt_finrank

Modified Mathlib/LinearAlgebra/Dimension/DivisionRing.lean

deleted theorem finrank_range_le_card

deleted theorem finrank_span_eq_card

deleted theorem finrank_span_finset_eq_card

deleted theorem finrank_span_finset_le_card

deleted theorem finrank_span_le_card

deleted theorem finrank_span_set_eq_card

deleted theorem rank_span_le

deleted theorem span_lt_of_subset_of_card_lt_finrank

deleted theorem span_lt_top_of_card_lt_finrank

Created Mathlib/LinearAlgebra/Dimension/Localization.lean

added theorem IsLocalizedModule.lift_rank_eq

added theorem IsLocalizedModule.rank_eq

added theorem rank_quotient_add_rank_of_isDomain

Modified Mathlib/NumberTheory/NumberField/Basic.lean