Commit 2024-10-24 16:57 97153441

View on Github →

feat: miscellaneous results about finrank (#18064) From flt-regular.

Estimated changes

Modified Mathlib/LinearAlgebra/Dimension/RankNullity.lean

added theorem LinearMap.lift_rank_eq_of_surjective

added theorem LinearMap.lift_rank_range_add_rank_ker

added theorem LinearMap.rank_eq_of_surjective

added theorem LinearMap.rank_range_add_rank_ker

added theorem Submodule.exists_of_finrank_lt

added theorem Submodule.exists_smul_not_mem_of_rank_lt

added theorem Submodule.finrank_quotient

added theorem Submodule.finrank_quotient_add_finrank

added theorem Submodule.rank_quotient_add_rank

deleted theorem exists_smul_not_mem_of_rank_lt

deleted theorem lift_rank_eq_of_surjective

deleted theorem lift_rank_range_add_rank_ker

deleted theorem rank_eq_of_surjective

deleted theorem rank_quotient_add_rank

deleted theorem rank_range_add_rank_ker

Modified Mathlib/LinearAlgebra/FiniteDimensional.lean

deleted theorem Submodule.finrank_quotient_add_finrank

Modified Mathlib/NumberTheory/RamificationInertia.lean