Theorems · Theorem · linear algebra

LinearMap.ofIsCompl_right_apply

Deprecated since 2026-05-16Use LinearMap.ofIsCompl_apply_right instead.

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

Alias of LinearMap.ofIsCompl_apply_right.

Defined in

Mathlib.LinearAlgebra.Projection

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModuleAddCommGroupModule