Commit 2026-04-03 14:10 5b6d247b

View on Github →

refactor(LinearAlgebra/LinearPMap): generalize (partially) to semilinear maps (#36721) replace LinearPMap.toFun : domain →ₗ[R] F by domain →ₛₗ[σ] F, in order to allow semilinear maps, in particular conjugate-linear maps.

Estimated changes

modified structure Module.Baer.ExtensionOf
modified def LinearMap.compPMap
modified theorem LinearMap.compPMap_apply
modified def LinearMap.toPMap
modified theorem LinearMap.toPMap_apply
modified theorem LinearMap.toPMap_domain
modified theorem LinearPMap.add_apply
modified theorem LinearPMap.add_domain
modified theorem LinearPMap.coe_smul
modified theorem LinearPMap.coe_vadd
modified def LinearPMap.comp
modified def LinearPMap.coprod
modified theorem LinearPMap.coprod_apply
modified theorem LinearPMap.dExt
modified theorem LinearPMap.dExt_iff
modified theorem LinearPMap.domRestrict_le
modified theorem LinearPMap.domain_mono
modified theorem LinearPMap.domain_sSup
modified theorem LinearPMap.domain_sup
modified def LinearPMap.eqLocus
modified theorem LinearPMap.exists_of_le
modified theorem LinearPMap.ext'
modified theorem LinearPMap.ext
modified theorem LinearPMap.ext_iff
modified theorem LinearPMap.fst_apply
modified def LinearPMap.graph
modified theorem LinearPMap.le_of_eqLocus_ge
modified theorem LinearPMap.map_add
modified theorem LinearPMap.map_neg
modified theorem LinearPMap.map_smul
modified theorem LinearPMap.map_sub
modified theorem LinearPMap.map_zero
modified theorem LinearPMap.mem_graph
modified theorem LinearPMap.mem_graph_iff'
modified theorem LinearPMap.mem_graph_iff
modified theorem LinearPMap.mk_apply
modified theorem LinearPMap.neg_apply
modified theorem LinearPMap.neg_domain
modified theorem LinearPMap.smul_apply
modified theorem LinearPMap.smul_domain
modified theorem LinearPMap.snd_apply
modified theorem LinearPMap.sub_apply
modified theorem LinearPMap.sub_domain
modified theorem LinearPMap.sup_apply
modified def LinearPMap.toFun'
modified theorem LinearPMap.toFun_eq_coe
modified theorem LinearPMap.vadd_apply
modified theorem LinearPMap.vadd_domain
modified theorem LinearPMap.zero_apply
modified theorem LinearPMap.zero_domain
modified structure LinearPMap