Theorems · Definition · linear algebra

Submodule.quotientEquivOfIsCompl

{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 → (E ⧸ p) ≃ₗ[R] ↥q

If q is a complement of p, then M ⧸ p ≃ q. The forward direction sends a quotient class to its projection onto q along p; the backward direction sends an element of q to its class in M ⧸ p.

Defined in

Mathlib.LinearAlgebra.Projection

Cited by

23 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModule