Mathlib Changelog
v4
Changelog
About
Github
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