Commit 2023-02-13 06:07 22222159

View on Github →

feat: port LinearAlgebra.Basic (#1979)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Basic.lean

added def Equiv.toLinearEquiv

added theorem Finsupp.LinearEquiv.finsuppUnique_apply

added theorem Finsupp.LinearEquiv.finsuppUnique_symm_apply

added theorem Finsupp.linearEquivFunOnFinite_single

added theorem Finsupp.linearEquivFunOnFinite_symm_coe

added theorem Finsupp.linearEquivFunOnFinite_symm_single

added theorem Finsupp.smul_sum

added theorem Finsupp.sum_smul_index_linearMap'

added theorem IsLinearMap.isLinearMap_add

added theorem IsLinearMap.isLinearMap_sub

added def LinearEquiv.arrowCongr

added theorem LinearEquiv.arrowCongr_apply

added theorem LinearEquiv.arrowCongr_comp

added theorem LinearEquiv.arrowCongr_symm_apply

added theorem LinearEquiv.arrowCongr_trans

added theorem LinearEquiv.coe_curry

added theorem LinearEquiv.coe_curry_symm

added theorem LinearEquiv.coe_neg

added theorem LinearEquiv.coe_ofEq_apply

added theorem LinearEquiv.coe_ofTop_symm_apply

added theorem LinearEquiv.coe_zero

added def LinearEquiv.congrRight

added def LinearEquiv.conj

added theorem LinearEquiv.conj_apply

added theorem LinearEquiv.conj_apply_apply

added theorem LinearEquiv.conj_comp

added theorem LinearEquiv.conj_id

added theorem LinearEquiv.conj_trans

added theorem LinearEquiv.eq_bot_of_equiv

added def LinearEquiv.funCongrLeft

added theorem LinearEquiv.funCongrLeft_apply

added theorem LinearEquiv.funCongrLeft_comp

added theorem LinearEquiv.funCongrLeft_id

added theorem LinearEquiv.funCongrLeft_symm

added theorem LinearEquiv.ker_comp

added theorem LinearEquiv.map_dfinsupp_sum

added theorem LinearEquiv.map_dfinsupp_sumAddHom

added theorem LinearEquiv.map_eq_comap

added theorem LinearEquiv.map_finsupp_sum

added theorem LinearEquiv.map_neg

added theorem LinearEquiv.map_sub

added theorem LinearEquiv.map_sum

added def LinearEquiv.neg

added theorem LinearEquiv.neg_apply

added theorem LinearEquiv.ofBijective_apply

added def LinearEquiv.ofEq

added theorem LinearEquiv.ofEq_rfl

added theorem LinearEquiv.ofEq_symm

added theorem LinearEquiv.ofInjective_apply

added def LinearEquiv.ofLeftInverse

added theorem LinearEquiv.ofLeftInverse_apply

added theorem LinearEquiv.ofLeftInverse_symm_apply

added def LinearEquiv.ofLinear

added theorem LinearEquiv.ofLinear_apply

added theorem LinearEquiv.ofLinear_symm_apply

added def LinearEquiv.ofSubmodule'

added theorem LinearEquiv.ofSubmodule'_apply

added theorem LinearEquiv.ofSubmodule'_symm_apply

added theorem LinearEquiv.ofSubmodule'_toLinearMap

added def LinearEquiv.ofSubmodules

added theorem LinearEquiv.ofSubmodules_apply

added theorem LinearEquiv.ofSubmodules_symm_apply

added def LinearEquiv.ofTop

added theorem LinearEquiv.ofTop_apply

added theorem LinearEquiv.ofTop_symm_apply

added theorem LinearEquiv.range_comp

added def LinearEquiv.smulOfNeZero

added def LinearEquiv.smulOfUnit

added def LinearEquiv.submoduleMap

added theorem LinearEquiv.submoduleMap_apply

added theorem LinearEquiv.submoduleMap_symm_apply

added theorem LinearEquiv.symm_conj_apply

added theorem LinearEquiv.symm_neg

added theorem LinearEquiv.zero_apply

added theorem LinearEquiv.zero_symm

added def LinearMap.applyₗ'

added def LinearMap.applyₗ

added def LinearMap.codRestrict

added theorem LinearMap.codRestrict_apply

added theorem LinearMap.coeFn_sum

added theorem LinearMap.coe_dfinsupp_sum

added theorem LinearMap.coe_finsupp_sum

added theorem LinearMap.coe_pow

added theorem LinearMap.coe_smulRight

added theorem LinearMap.comap_codRestrict

added theorem LinearMap.comap_injective

added theorem LinearMap.comap_le_comap_iff

added theorem LinearMap.commute_pow_left_of_commute

added def LinearMap.compRight

added theorem LinearMap.compRight_apply

added theorem LinearMap.comp_assoc

added theorem LinearMap.comp_codRestrict

added theorem LinearMap.comp_ker_subtype

added theorem LinearMap.dfinsupp_sum_apply

added theorem LinearMap.disjoint_ker'

added theorem LinearMap.disjoint_ker

added def LinearMap.domRestrict'

added theorem LinearMap.domRestrict'_apply

added def LinearMap.domRestrict

added theorem LinearMap.domRestrict_apply

added def LinearMap.eqLocus

added theorem LinearMap.eqLocus_eq_ker_sub

added theorem LinearMap.eqLocus_same

added theorem LinearMap.eqLocus_toAddSubmonoid

added def LinearMap.evalAddMonoidHom

added theorem LinearMap.finsupp_sum_apply

added def LinearMap.funLeft

added theorem LinearMap.funLeft_apply

added theorem LinearMap.funLeft_comp

added theorem LinearMap.funLeft_id

added theorem LinearMap.funLeft_injective_of_surjective

added theorem LinearMap.funLeft_surjective_of_injective

added theorem LinearMap.id_pow

added theorem LinearMap.infᵢ_invariant

added theorem LinearMap.injOn_of_disjoint_ker

added theorem LinearMap.injective_of_iterate_injective

added def LinearMap.iterateKer

added def LinearMap.iterateRange

added theorem LinearMap.iterate_bijective

added theorem LinearMap.iterate_injective

added theorem LinearMap.iterate_succ

added theorem LinearMap.iterate_surjective

added def LinearMap.ker

added theorem LinearMap.ker_codRestrict

added theorem LinearMap.ker_comp

added theorem LinearMap.ker_comp_of_ker_eq_bot

added theorem LinearMap.ker_eq_bot'

added theorem LinearMap.ker_eq_bot

added theorem LinearMap.ker_eq_bot_of_cancel

added theorem LinearMap.ker_eq_bot_of_injective

added theorem LinearMap.ker_eq_bot_of_inverse

added theorem LinearMap.ker_eq_top

added theorem LinearMap.ker_id

added theorem LinearMap.ker_le_iff

added theorem LinearMap.ker_le_ker_comp

added theorem LinearMap.ker_rangeRestrict

added theorem LinearMap.ker_restrict

added theorem LinearMap.ker_smul'

added theorem LinearMap.ker_smul

added theorem LinearMap.ker_toAddSubgroup

added theorem LinearMap.ker_toAddSubmonoid

added theorem LinearMap.ker_zero

added theorem LinearMap.le_ker_iff_map

added theorem LinearMap.map_codRestrict

added theorem LinearMap.map_coe_ker

added theorem LinearMap.map_dfinsupp_sum

added theorem LinearMap.map_dfinsupp_sumAddHom

added theorem LinearMap.map_finsupp_sum

added theorem LinearMap.map_le_range

added theorem LinearMap.map_sum

added theorem LinearMap.mem_eqLocus

added theorem LinearMap.mem_ker

added theorem LinearMap.mem_range

added theorem LinearMap.mem_range_self

added theorem LinearMap.mem_submoduleImage

added theorem LinearMap.mem_submoduleImage_of_le

added theorem LinearMap.pi_apply_eq_sum_univ

added theorem LinearMap.pow_apply

added theorem LinearMap.pow_apply_mem_of_forall_mem

added theorem LinearMap.pow_map_zero_of_le

added theorem LinearMap.pow_restrict

added def LinearMap.range

added def LinearMap.rangeRestrict

added theorem LinearMap.range_codRestrict

added theorem LinearMap.range_coe

added theorem LinearMap.range_comp

added theorem LinearMap.range_comp_le_range

added theorem LinearMap.range_comp_of_range_eq_top

added theorem LinearMap.range_eq_bot

added theorem LinearMap.range_eq_map

added theorem LinearMap.range_eq_top

added theorem LinearMap.range_id

added theorem LinearMap.range_le_bot_iff

added theorem LinearMap.range_le_iff_comap

added theorem LinearMap.range_le_ker_iff

added theorem LinearMap.range_neg

added theorem LinearMap.range_rangeRestrict

added theorem LinearMap.range_smul'

added theorem LinearMap.range_smul

added theorem LinearMap.range_toAddSubgroup

added theorem LinearMap.range_toAddSubmonoid

added theorem LinearMap.range_zero

added def LinearMap.restrict

added theorem LinearMap.restrict_apply

added theorem LinearMap.restrict_coe_apply

added theorem LinearMap.restrict_eq_codRestrict_domRestrict

added theorem LinearMap.restrict_eq_domRestrict_codRestrict

added def LinearMap.ringLmapEquivSelf

added def LinearMap.smulRight

added theorem LinearMap.smulRight_apply

added def LinearMap.smulRightₗ

added theorem LinearMap.smulRightₗ_apply

added theorem LinearMap.sub_mem_ker_iff

added def LinearMap.submoduleImage

added theorem LinearMap.submoduleImage_apply_ofLe

added theorem LinearMap.submodule_pow_eq_zero_of_pow_eq_zero

added theorem LinearMap.subtype_comp_codRestrict

added theorem LinearMap.subtype_comp_restrict

added theorem LinearMap.sum_apply

added theorem LinearMap.surjective_of_iterate_surjective

added def LinearMap.toAddMonoidHom'

added theorem LinearMapClass.ker_eq_bot

added def Submodule.MapSubtype.orderEmbedding

added def Submodule.MapSubtype.relIso

added theorem Submodule.apply_coe_mem_map

added theorem Submodule.coe_equivMapOfInjective_apply

added theorem Submodule.coe_ofLe

added def Submodule.comap

added def Submodule.comapSubtypeEquivOfLe

added theorem Submodule.comapSubtypeEquivOfLe_apply_coe

added theorem Submodule.comap_bot

added theorem Submodule.comap_coe

added theorem Submodule.comap_comp

added theorem Submodule.comap_equiv_eq_map_symm

added theorem Submodule.comap_id

added theorem Submodule.comap_inf

added theorem Submodule.comap_inf_map_of_injective

added theorem Submodule.comap_infᵢ

added theorem Submodule.comap_infᵢ_map_of_injective

added theorem Submodule.comap_injective_of_surjective

added theorem Submodule.comap_le_comap_iff_of_surjective

added theorem Submodule.comap_le_comap_smul

added theorem Submodule.comap_map_eq_of_injective

added theorem Submodule.comap_mono

added theorem Submodule.comap_smul'

added theorem Submodule.comap_smul

added theorem Submodule.comap_strictMono_of_surjective

added theorem Submodule.comap_subtype_eq_top

added theorem Submodule.comap_subtype_self

added theorem Submodule.comap_sup_map_of_injective

added theorem Submodule.comap_supᵢ_map_of_injective

added theorem Submodule.comap_surjective_of_injective

added theorem Submodule.comap_top

added theorem Submodule.comap_zero

added def Submodule.compatibleMaps

added theorem Submodule.disjoint_iff_comap_eq_bot

added theorem Submodule.eq_zero_of_bot_submodule

added def Submodule.equivSubtypeMap

added theorem Submodule.equivSubtypeMap_apply

added theorem Submodule.equivSubtypeMap_symm_apply

added theorem Submodule.gc_map_comap

added def Submodule.gciMapComap

added def Submodule.giMapComap

added theorem Submodule.inf_comap_le_comap_add

added theorem Submodule.ker_ofLe

added theorem Submodule.ker_subtype

added theorem Submodule.le_comap_map

added theorem Submodule.le_comap_pow_of_le_comap

added def Submodule.map

added theorem Submodule.map_add_le

added theorem Submodule.map_bot

added theorem Submodule.map_coe

added theorem Submodule.map_comap_eq

added theorem Submodule.map_comap_eq_of_surjective

added theorem Submodule.map_comap_eq_self

added theorem Submodule.map_comap_le

added theorem Submodule.map_comap_subtype

added theorem Submodule.map_comp

added theorem Submodule.map_equiv_eq_comap_symm

added theorem Submodule.map_id

added theorem Submodule.map_inf_comap_of_surjective

added theorem Submodule.map_inf_eq_map_inf_comap

added theorem Submodule.map_infᵢ_comap_of_surjective

added theorem Submodule.map_injective_of_injective

added theorem Submodule.map_le_iff_le_comap

added theorem Submodule.map_le_map_iff_of_injective

added theorem Submodule.map_mono

added theorem Submodule.map_smul'

added theorem Submodule.map_smul

added theorem Submodule.map_strictMono_of_injective

added theorem Submodule.map_subtype_embedding_eq

added theorem Submodule.map_subtype_le

added theorem Submodule.map_subtype_range_ofLe

added theorem Submodule.map_subtype_top

added theorem Submodule.map_sup

added theorem Submodule.map_sup_comap_of_surjective

added theorem Submodule.map_supᵢ

added theorem Submodule.map_supᵢ_comap_of_sujective

added theorem Submodule.map_surjective_of_surjective

added theorem Submodule.map_symm_eq_iff

added theorem Submodule.map_toAddSubmonoid

added theorem Submodule.map_to_add_submonoid'

added theorem Submodule.map_top

added theorem Submodule.map_zero

added theorem Submodule.mem_comap

added theorem Submodule.mem_left_iff_eq_zero_of_disjoint

added theorem Submodule.mem_map

added theorem Submodule.mem_map_equiv

added theorem Submodule.mem_map_of_mem

added theorem Submodule.mem_right_iff_eq_zero_of_disjoint

added theorem Submodule.neg_coe

added theorem Submodule.nontrivial_iff

added def Submodule.ofLe

added theorem Submodule.ofLe_apply

added theorem Submodule.ofLe_injective

added def Submodule.orderIsoMapComap

added theorem Submodule.orderIsoMapComap_apply'

added theorem Submodule.orderIsoMapComap_symm_apply'

added theorem Submodule.range_map_nonempty

added theorem Submodule.range_ofLe

added theorem Submodule.range_subtype

added theorem Submodule.subsingleton_iff

added theorem Submodule.subtype_comp_ofLe

added def addMonoidHomLequivInt

added def addMonoidHomLequivNat

added theorem pi_eq_sum_univ