Commit 2023-04-25 11:42 66535631

View on Github →

feat: port LinearAlgebra.FiniteDimensional (#3466)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/FiniteDimensional.lean

added theorem CompleteLattice.Independent.subtype_ne_bot_le_finrank

added theorem CompleteLattice.Independent.subtype_ne_bot_le_finrank_aux

added theorem FiniteDimensional.basisSingleton_apply

added theorem FiniteDimensional.basisUnique.repr_eq_zero_iff

added theorem FiniteDimensional.cardinal_mk_le_finrank_of_linearIndependent

added theorem FiniteDimensional.eq_of_le_of_finrank_eq

added theorem FiniteDimensional.eq_of_le_of_finrank_le

added theorem FiniteDimensional.eq_top_of_finrank_eq

added theorem FiniteDimensional.exists_nontrivial_relation_of_rank_lt_card

added theorem FiniteDimensional.exists_nontrivial_relation_sum_zero_of_rank_succ_lt_card

added theorem FiniteDimensional.exists_relation_sum_zero_pos_coefficient_of_rank_succ_lt_card

added theorem FiniteDimensional.fact_finiteDimensional_of_finrank_eq_succ

added theorem FiniteDimensional.finiteDimensional_iff_of_rank_eq_nsmul

added theorem FiniteDimensional.finiteDimensional_of_finrank

added theorem FiniteDimensional.finiteDimensional_of_finrank_eq_succ

added theorem FiniteDimensional.finite_of_finite

added theorem FiniteDimensional.finrank_eq_card_basis'

added theorem FiniteDimensional.finrank_eq_rank'

added theorem FiniteDimensional.finrank_of_infinite_dimensional

added theorem FiniteDimensional.finrank_pos

added theorem FiniteDimensional.finrank_pos_iff

added theorem FiniteDimensional.finrank_pos_iff_exists_ne_zero

added theorem FiniteDimensional.finrank_zero_iff

added theorem FiniteDimensional.finset_card_le_finrank_of_linearIndependent

added theorem FiniteDimensional.fintype_card_le_finrank_of_linearIndependent

added theorem FiniteDimensional.lt_aleph0_of_linearIndependent

added theorem FiniteDimensional.not_linearIndependent_of_infinite

added theorem FiniteDimensional.of_finite_basis

added theorem FiniteDimensional.of_fintype_basis

added theorem FiniteDimensional.of_injective

added theorem FiniteDimensional.of_surjective

added theorem FiniteDimensional.range_basisSingleton

added theorem FiniteDimensional.span_of_finite

added def FiniteDimensional

added theorem LinearEquiv.coe_ofInjectiveEndo

added theorem LinearEquiv.ofInjectiveEndo_left_inv

added theorem LinearEquiv.ofInjectiveEndo_right_inv

added theorem LinearIndependent.finite

added theorem LinearMap.comp_eq_id_comm

added theorem LinearMap.finiteDimensional_of_surjective

added theorem LinearMap.finrank_range_add_finrank_ker

added theorem LinearMap.injective_iff_surjective

added theorem LinearMap.injective_iff_surjective_of_finrank_eq_finrank

added theorem LinearMap.isUnit_iff_ker_eq_bot

added theorem LinearMap.isUnit_iff_range_eq_top

added theorem LinearMap.ker_eq_bot_iff_range_eq_top

added theorem LinearMap.ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank

added theorem LinearMap.linearEquivOfInjective_apply

added theorem LinearMap.mul_eq_one_comm

added theorem LinearMap.mul_eq_one_of_mul_eq_one

added theorem LinearMap.surjective_of_injective

added theorem Module.End.exists_ker_pow_eq_ker_pow_succ

added theorem Module.End.ker_pow_constant

added theorem Module.End.ker_pow_eq_ker_pow_finrank_of_le

added theorem Module.End.ker_pow_le_ker_pow_finrank

added theorem Module.finrank_le_one_iff_top_isPrincipal

added theorem Set.finrank_mono

added theorem Subalgebra.bot_eq_top_iff_finrank_eq_one

added theorem Subalgebra.bot_eq_top_iff_rank_eq_one

added theorem Subalgebra.eq_bot_of_finrank_one

added theorem Subalgebra.eq_bot_of_rank_le_one

added theorem Subalgebra.finiteDimensional_toSubmodule

added theorem Subalgebra.finrank_eq_one_iff

added theorem Subalgebra.isSimpleOrder_of_finrank

added theorem Subalgebra.rank_eq_one_iff

added theorem Submodule.eq_top_of_disjoint

added theorem Submodule.eq_top_of_finrank_eq

added theorem Submodule.fg_iff_finiteDimensional

added theorem Submodule.finiteDimensional_of_le

added theorem Submodule.finrank_add_eq_of_isCompl

added theorem Submodule.finrank_add_le_finrank_add_finrank

added theorem Submodule.finrank_le_one_iff_isPrincipal

added theorem Submodule.finrank_lt

added theorem Submodule.finrank_lt_finrank_of_lt

added theorem Submodule.finrank_mono

added theorem Submodule.finrank_quotient_add_finrank

added theorem Submodule.finrank_strictMono

added theorem Submodule.finrank_sup_add_finrank_inf_eq

added theorem bot_eq_top_of_rank_eq_zero

added theorem cardinal_lt_aleph0_of_finiteDimensional

added theorem cardinal_mk_eq_cardinal_mk_field_pow_rank

added theorem coe_basisOfLinearIndependentOfCardEqFinrank

added theorem coe_finsetBasisOfLinearIndependentOfCardEqFinrank

added theorem coe_setBasisOfLinearIndependentOfCardEqFinrank

added theorem finiteDimensional_of_rank_eq_nat

added theorem finiteDimensional_of_rank_eq_one

added theorem finiteDimensional_of_rank_eq_zero

added theorem finrank_eq_one_iff'

added theorem finrank_eq_one_iff

added theorem finrank_eq_one_iff_of_nonzero'

added theorem finrank_eq_one_iff_of_nonzero

added theorem finrank_eq_zero

added theorem finrank_eq_zero_of_rank_eq_zero

added theorem finrank_le_one_iff

added theorem finrank_span_singleton

added theorem finrank_zero_iff_forall_zero

added theorem is_simple_module_of_finrank_eq_one

added theorem rank_eq_zero

added theorem span_eq_top_of_linearIndependent_of_card_eq_finrank

added theorem surjective_of_nonzero_of_finrank_eq_one

Modified Mathlib/Tactic.lean