Theorems · Theorem · linear algebra

LinearMap.surjective_comp_subtype_of_isComplemented

∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p : Submodule R E}
  {M : Type u_6} [inst_3 : AddCommMonoid M],
  IsComplemented p → ∀ [inst_4 : Module R M], Function.Surjective fun f => f ∘ₗ p.subtype

Defined in

Mathlib.LinearAlgebra.Projection

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModuleAddCommMonoidModule