Theorems · Theorem · linear algebra

LinearMap.restrict_sub

∀ {R : Type u_10} {R₂ : Type u_11} {M : Type u_12} {M₂ : Type u_13} [inst : Ring R] [inst_1 : Ring R₂] {σ₁₂ : R →+* R₂}
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {p : Submodule R M}
  {q : Submodule R₂ M₂} {f g : M →ₛₗ[σ₁₂] M₂} (hf : Set.MapsTo ⇑f ↑p ↑q) (hg : Set.MapsTo ⇑g ↑p ↑q)
  (hfg : optParam (Set.MapsTo ⇑(f - g) ↑p ↑q) ⋯), f.restrict hf - g.restrict hg = (f - g).restrict hfg

Defined in

Mathlib.Algebra.Module.Submodule.LinearMap

Cited by

3 results in Mathlib

Foundations

Depth 29 from the axioms · uses propext, Quot.sound

Assumes

RingRingAddCommGroupAddCommGroupModuleModule