Commit 2023-02-24 00:08 b00fce6d

View on Github →

feat: port LinearAlgebra.LinearPMap (#2422)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/LinearPMap.lean

added def LinearMap.compPMap

added theorem LinearMap.compPMap_apply

added def LinearMap.toPMap

added theorem LinearMap.toPMap_apply

added theorem LinearPMap.apply_comp_ofLe

added def LinearPMap.codRestrict

added theorem LinearPMap.coe_smul

added theorem LinearPMap.coe_vadd

added def LinearPMap.comp

added def LinearPMap.coprod

added theorem LinearPMap.coprod_apply

added def LinearPMap.domRestrict

added theorem LinearPMap.domRestrict_apply

added theorem LinearPMap.domRestrict_domain

added theorem LinearPMap.domRestrict_le

added theorem LinearPMap.domain_mkSpanSingleton

added theorem LinearPMap.domain_mono

added theorem LinearPMap.domain_sup

added theorem LinearPMap.domain_supSpanSingleton

added def LinearPMap.eqLocus

added theorem LinearPMap.eq_of_eq_graph

added theorem LinearPMap.eq_of_le_of_domain_eq

added theorem LinearPMap.exists_of_le

added theorem LinearPMap.ext'

added theorem LinearPMap.ext

added theorem LinearPMap.ext_iff

added theorem LinearPMap.fst_apply

added def LinearPMap.graph

added theorem LinearPMap.graph_fst_eq_zero_snd

added theorem LinearPMap.image_iff

added theorem LinearPMap.le_graph_iff

added theorem LinearPMap.le_graph_of_le

added theorem LinearPMap.le_of_eqLocus_ge

added theorem LinearPMap.le_of_le_graph

added theorem LinearPMap.map_add

added theorem LinearPMap.map_neg

added theorem LinearPMap.map_smul

added theorem LinearPMap.map_sub

added theorem LinearPMap.map_zero

added theorem LinearPMap.mem_domain_iff

added theorem LinearPMap.mem_domain_iff_of_eq_graph

added theorem LinearPMap.mem_domain_of_mem_graph

added theorem LinearPMap.mem_graph

added theorem LinearPMap.mem_graph_iff'

added theorem LinearPMap.mem_graph_iff

added theorem LinearPMap.mem_graph_snd_inj'

added theorem LinearPMap.mem_graph_snd_inj

added theorem LinearPMap.mem_range_iff

added theorem LinearPMap.mkSpanSingleton'_apply

added theorem LinearPMap.mkSpanSingleton'_apply_self

added theorem LinearPMap.mkSpanSingleton_apply

added theorem LinearPMap.mk_apply

added theorem LinearPMap.neg_apply

added theorem LinearPMap.neg_graph

added theorem LinearPMap.smul_apply

added theorem LinearPMap.smul_domain

added theorem LinearPMap.smul_graph

added theorem LinearPMap.snd_apply

added theorem LinearPMap.supSpanSingleton_apply_mk

added theorem LinearPMap.sup_apply

added theorem LinearPMap.sup_h_of_disjoint

added def LinearPMap.toFun'

added theorem LinearPMap.toFun_eq_coe

added theorem LinearPMap.vadd_apply

added theorem LinearPMap.vadd_domain

added structure LinearPMap

added theorem Submodule.existsUnique_from_graph

added theorem Submodule.mem_graph_toLinearPMap

added theorem Submodule.toLinearPMap_graph_eq

added theorem Submodule.valFromGraph_mem