Commit 2023-04-12 20:56 1e02adbd

View on Github →

feat: port LinearAlgebra.Finrank (#3378)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Finrank.lean

added theorem FiniteDimensional.Basis.subset_extend

added theorem FiniteDimensional.finrank_eq_card_basis

added theorem FiniteDimensional.finrank_eq_card_finset_basis

added theorem FiniteDimensional.finrank_eq_of_rank_eq

added theorem FiniteDimensional.finrank_fin_fun

added theorem FiniteDimensional.finrank_fintype_fun_eq_card

added theorem FiniteDimensional.finrank_le_finrank_of_rank_le_rank

added theorem FiniteDimensional.finrank_le_of_rank_le

added theorem FiniteDimensional.finrank_lt_of_rank_lt

added theorem FiniteDimensional.finrank_self

added theorem FiniteDimensional.finrank_zero_of_subsingleton

added theorem FiniteDimensional.nontrivial_of_finrank_eq_succ

added theorem FiniteDimensional.nontrivial_of_finrank_pos

added theorem FiniteDimensional.rank_lt_of_finrank_lt

added theorem LinearEquiv.finrank_eq

added theorem LinearEquiv.finrank_map_eq

added theorem LinearMap.finrank_range_of_inj

added theorem Subalgebra.finrank_bot

added theorem Subalgebra.finrank_toSubmodule

added theorem Subalgebra.rank_bot

added theorem Subalgebra.rank_toSubmodule

added theorem Subalgebra.rank_top

added theorem Submodule.lt_of_le_of_finrank_lt_finrank

added theorem Submodule.lt_top_of_finrank_lt_finrank

added theorem coe_basisOfTopLeSpanOfCardEqFinrank

added theorem finrank_bot

added theorem finrank_eq_one

added theorem finrank_eq_zero_of_basis_imp_false

added theorem finrank_eq_zero_of_basis_imp_not_finite

added theorem finrank_eq_zero_of_not_exists_basis

added theorem finrank_eq_zero_of_not_exists_basis_finite

added theorem finrank_eq_zero_of_not_exists_basis_finset

added theorem finrank_le_one

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 finrank_top

added theorem linearIndependent_iff_card_eq_finrank_span

added theorem linearIndependent_iff_card_le_finrank_span

added theorem linearIndependent_of_top_le_span_of_card_eq_finrank

added theorem span_lt_of_subset_of_card_lt_finrank

added theorem span_lt_top_of_card_lt_finrank

added theorem subalgebra_top_finrank_eq_submodule_top_finrank

added theorem subalgebra_top_rank_eq_submodule_top_rank