Theorems · Definition · linear algebra

LinearMap.equivProdOfSurjectiveOfIsCompl

{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] →
                {G : Type u_4} →
                  [inst_5 : AddCommGroup G] →
                    [inst_6 : Module R G] →
                      (f : E →ₗ[R] F) →
                        (g : E →ₗ[R] G) → f.range = ⊤ → g.range = ⊤ → IsCompl f.ker g.ker → E ≃ₗ[R] F × G

If f : E →ₗ[R] F and g : E →ₗ[R] G are two surjective linear maps and their kernels are complement of each other, then x ↦ (f x, g x) defines a linear equivalence E ≃ₗ[R] F × G.

Defined in

Mathlib.LinearAlgebra.Projection

Cited by

3 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModuleAddCommGroupModuleAddCommGroupModule