Commit 2023-04-10 07:27 afb1a7e2

View on Github →

feat: port LinearAlgebra.Dimension (#3354)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Dimension.lean

added theorem Basis.card_le_card_of_le

added theorem Basis.card_le_card_of_linearIndependent

added theorem Basis.card_le_card_of_linearIndependent_aux

added theorem Basis.card_le_card_of_submodule

added theorem Basis.finite_index_of_rank_lt_aleph0

added theorem Basis.finite_ofVectorSpaceIndex_of_rank_lt_aleph0

added def Basis.indexEquiv

added theorem Basis.le_span''

added theorem Basis.le_span

added theorem Basis.mk_eq_rank''

added theorem Basis.mk_eq_rank'.{m}

added theorem Basis.mk_eq_rank

added theorem Basis.mk_range_eq_rank

added theorem Basis.nonempty_fintype_index_of_rank_lt_aleph0

added def Basis.ofRankEqZero

added theorem Basis.ofRankEqZero_apply

added theorem CompleteLattice.Independent.subtype_ne_bot_le_rank

added theorem Ideal.rank_eq

added theorem LinearEquiv.lift_rank_eq

added theorem LinearEquiv.nonempty_equiv_iff_lift_rank_eq

added theorem LinearEquiv.nonempty_equiv_iff_rank_eq

added def LinearEquiv.ofLiftRankEq

added def LinearEquiv.ofRankEq

added theorem LinearEquiv.rank_eq

added theorem LinearEquiv.rank_map_eq

added theorem LinearIndependent.finite_of_isNoetherian

added theorem LinearIndependent.set_finite_of_isNoetherian

added theorem LinearMap.le_rank_iff_exists_linearIndependent

added theorem LinearMap.le_rank_iff_exists_linearIndependent_finset

added theorem LinearMap.lift_rank_le_of_injective

added def LinearMap.rank

added theorem LinearMap.rank_add_le

added theorem LinearMap.rank_comp_le_left

added theorem LinearMap.rank_comp_le_right

added theorem LinearMap.rank_finset_sum_le

added theorem LinearMap.rank_le_domain

added theorem LinearMap.rank_le_of_injective

added theorem LinearMap.rank_le_of_surjective

added theorem LinearMap.rank_le_range

added theorem LinearMap.rank_zero

added theorem Module.Free.rank_eq_card_chooseBasisIndex

added theorem Module.rank_le_one_iff_top_isPrincipal

added def Submodule.inductionOnRank

added theorem Submodule.rank_add_le_rank_add_rank

added theorem Submodule.rank_le_one_iff_isPrincipal

added theorem Submodule.rank_sup_add_rank_inf_eq

added def basisFintypeOfFiniteSpans

added theorem basis_le_span'

added theorem cardinal_le_rank_of_linearIndependent'

added theorem cardinal_le_rank_of_linearIndependent

added theorem cardinal_lift_le_rank_of_linearIndependent'

added theorem cardinal_lift_le_rank_of_linearIndependent

added theorem exists_mem_ne_zero_of_rank_pos

added def finDimVectorspaceEquiv

added theorem infinite_basis_le_maximal_linearIndependent'

added theorem infinite_basis_le_maximal_linearIndependent

added theorem le_rank_iff_exists_linearIndependent

added theorem le_rank_iff_exists_linearIndependent_finset

added theorem lift_rank_map_le

added theorem lift_rank_range_le

added def linearIndependentFintypeOfLeSpanFintype

added theorem linearIndependent_le_basis

added theorem linearIndependent_le_infinite_basis

added theorem linearIndependent_le_span'

added theorem linearIndependent_le_span

added theorem linearIndependent_le_span_aux'

added theorem maximal_linearIndependent_eq_infinite_basis

added theorem mk_eq_mk_of_basis'

added theorem mk_eq_mk_of_basis

added theorem nonempty_linearEquiv_of_lift_rank_eq

added theorem nonempty_linearEquiv_of_rank_eq

added theorem rank_add_rank_split

added theorem rank_bot

added theorem rank_eq_card_basis

added theorem rank_eq_of_injective

added theorem rank_eq_of_surjective

added theorem rank_fin_fun

added theorem rank_fun'

added theorem rank_fun

added theorem rank_fun_eq_lift_mul

added theorem rank_le

added theorem rank_le_of_submodule

added theorem rank_le_one_iff

added theorem rank_map_le

added theorem rank_pi

added theorem rank_pos

added theorem rank_pos_iff_exists_ne_zero

added theorem rank_pos_iff_nontrivial

added theorem rank_prod'

added theorem rank_prod

added theorem rank_punit

added theorem rank_quotient_add_rank

added theorem rank_quotient_le

added theorem rank_range_add_rank_ker

added theorem rank_range_le

added theorem rank_range_of_surjective

added theorem rank_self

added theorem rank_span

added theorem rank_span_le

added theorem rank_span_of_finset

added theorem rank_span_set

added theorem rank_submodule_le

added theorem rank_submodule_le_one_iff'

added theorem rank_submodule_le_one_iff

added theorem rank_subsingleton

added theorem rank_top

added theorem rank_zero_iff

added theorem rank_zero_iff_forall_zero

added theorem union_support_maximal_linearIndependent_eq_range_basis