Basic lemmas on partial linear maps #
General lemmas on LinearPMap that Mathlib does not provide.
Main results #
LinearPMap.congr_fun: the value-level part ofLinearPMap.ext_iff, with the two domain memberships as explicit arguments.LinearPMap.neg_smulandLinearPMap.smul_neg: a negation moves through a scalar multiple.
theorem
LinearPMap.congr_fun
{R : Type u_1}
{S : Type u_2}
{E : Type u_3}
{F : Type u_4}
[Ring R]
[Ring S]
{σ : R →+* S}
[AddCommGroup E]
[Module R E]
[AddCommGroup F]
[Module S F]
{f g : E →ₛₗ.[σ] F}
(h : f = g)
{x : E}
(hf : x ∈ f.domain)
(hg : x ∈ g.domain)
:
Equal partial linear maps take equal values: the value-level part of LinearPMap.ext_iff,
with the two domain memberships as explicit arguments.
@[simp]
theorem
LinearPMap.neg_smul
{R : Type u_1}
{S : Type u_2}
{E : Type u_3}
{F : Type u_4}
[Ring R]
[Ring S]
{σ : R →+* S}
[AddCommGroup E]
[Module R E]
[AddCommGroup F]
[Module S F]
{M : Type u_5}
[Ring M]
[Module M F]
[SMulCommClass S M F]
(c : M)
(A : E →ₛₗ.[σ] F)
:
Negating the scalar negates the scalar multiple of a partial linear map (LinearPMap is not a
module, so this is not an instance of neg_smul).
@[simp]
theorem
LinearPMap.smul_neg
{R : Type u_1}
{S : Type u_2}
{E : Type u_3}
{F : Type u_4}
[Ring R]
[Ring S]
{σ : R →+* S}
[AddCommGroup E]
[Module R E]
[AddCommGroup F]
[Module S F]
{M : Type u_5}
[Monoid M]
[DistribMulAction M F]
[SMulCommClass S M F]
(c : M)
(A : E →ₛₗ.[σ] F)
:
Negating the map negates the scalar multiple of a partial linear map.