Commit 2025-01-20 13:22 3368abb8

View on Github →

chore(LinearAlgebra): generalize results on ranks to semirings (#20774)

Estimated changes

Modified Mathlib/FieldTheory/CardinalEmb.lean

Modified Mathlib/FieldTheory/Relrank.lean

Modified Mathlib/LinearAlgebra/Basis/Basic.lean

Modified Mathlib/LinearAlgebra/Basis/Cardinality.lean

Modified Mathlib/LinearAlgebra/Dimension/Basic.lean

modified theorem lift_rank_eq_of_equiv_equiv

modified theorem lift_rank_le_of_injective_injective

added theorem lift_rank_le_of_injective_injectiveₛ

modified theorem lift_rank_le_of_surjective_injective

modified theorem rank_eq_of_equiv_equiv

modified theorem rank_le_of_injective_injective

added theorem rank_le_of_injective_injectiveₛ

modified theorem rank_le_of_surjective_injective

Modified Mathlib/LinearAlgebra/Dimension/Constructions.lean

modified theorem LinearIndependent.union_of_quotient

modified theorem Module.finrank_directSum

modified theorem Submodule.finrank_quotient_le

modified theorem rank_directSum

modified theorem rank_fun

Modified Mathlib/LinearAlgebra/Dimension/Finrank.lean

Modified Mathlib/LinearAlgebra/Dimension/Free.lean

Modified Mathlib/LinearAlgebra/Dimension/RankNullity.lean

Modified Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean

modified def Submodule.inductionOnRank

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

modified theorem LinearIndependent.map_of_surjective_injective

added theorem LinearIndependent.map_of_surjective_injectiveₛ