Theorems · Theorem · linear algebra

LinearMap.ofIsCompl_add

∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {p q : Submodule R E} (h : IsCompl p q) {φ₁ φ₂ : ↥p →ₗ[R] F}
  {ψ₁ ψ₂ : ↥q →ₗ[R] F},
  LinearMap.ofIsCompl h (φ₁ + φ₂) (ψ₁ + ψ₂) = LinearMap.ofIsCompl h φ₁ ψ₁ + LinearMap.ofIsCompl h φ₂ ψ₂

Defined in

Mathlib.LinearAlgebra.Projection

Cited by

1 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingAddCommGroupModuleAddCommGroupModule