Theorems · Definition · linear algebra

LinearPMap.sup

{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] →
                    [inst_5 : Module S F] →
                      (f g : E →ₛₗ.[σ] F) → (∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y) → E →ₛₗ.[σ] F

Given two partial linear maps that agree on the intersection of their domains, f.sup g h is the unique partial linear map on f.domain ⊔ g.domain that agrees with f and g.

Defined in

Mathlib.LinearAlgebra.LinearPMap

Cited by

6 results in Mathlib

Foundations

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

Assumes

RingRingAddCommGroupModuleAddCommGroupModule