Theorems · Theorem · linear algebra

LinearMap.ofIsCompl_apply_left

∀ {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} (u : ↥p), (LinearMap.ofIsCompl h φ ψ) ↑u = φ u

Defined in

Mathlib.LinearAlgebra.Projection

Cited by

5 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModuleAddCommGroupModule