Theorems · Definition · linear algebra

LinearPMap.coprod

{R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} →
                  [inst_4 : AddCommGroup F] →
                    {G : Type u_6} →
                      [inst_5 : AddCommGroup G] →
                        [inst_6 : Module R F] → [inst_7 : Module S G] → (E →ₛₗ.[σ] G) → (F →ₛₗ.[σ] G) → E × F →ₛₗ.[σ] G

f.coprod g is the partially defined linear map defined on f.domain × g.domain, and sending p to f p.1 + g p.2.

Defined in

Mathlib.LinearAlgebra.LinearPMap

Cited by

2 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Quot.sound

Assumes

RingRingAddCommGroupModuleAddCommGroupAddCommGroupModuleModule