Theorems · Definition · linear algebra

Submodule.prodEquivOfIsCompl

{R : Type u_1} →
  [inst : Ring R] →
    {E : Type u_2} →
      [inst_1 : AddCommGroup E] → [inst_2 : Module R E] → (p q : Submodule R E) → IsCompl p q → (↥p × ↥q) ≃ₗ[R] E

If q is a complement of p, then p × q is isomorphic to E.

Defined in

Mathlib.LinearAlgebra.Projection

Cited by

35 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModule