Commit 2023-04-16 11:41 2d048efe

View on Github →

feat: port LinearAlgebra.FreeModule.Finite.Rank (#3455)

Estimated changes

Modified Mathlib.lean

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

added theorem FiniteDimensional.Submodule.finrank_map_subtype_eq

added theorem FiniteDimensional.finrank_directSum

added theorem FiniteDimensional.finrank_eq_card_chooseBasisIndex

added theorem FiniteDimensional.finrank_eq_rank

added theorem FiniteDimensional.finrank_finsupp

added theorem FiniteDimensional.finrank_matrix

added theorem FiniteDimensional.finrank_pi

added theorem FiniteDimensional.finrank_pi_fintype

added theorem FiniteDimensional.finrank_prod

added theorem FiniteDimensional.finrank_tensorProduct

added theorem FiniteDimensional.nonempty_linearEquiv_iff_finrank_eq

added theorem FiniteDimensional.nonempty_linearEquiv_of_finrank_eq

added theorem FiniteDimensional.rank_lt_aleph0

added theorem LinearMap.finrank_le_finrank_of_injective

added theorem LinearMap.finrank_range_le

added theorem Submodule.finrank_le

added theorem Submodule.finrank_le_finrank_of_le

added theorem Submodule.finrank_map_le

added theorem Submodule.finrank_quotient_le