Theorems · Definition · linear algebra

LinearPMap.supSpanSingleton

{E : Type u_4} →
  [inst : AddCommGroup E] →
    {F : Type u_5} →
      [inst_1 : AddCommGroup F] →
        {K : Type u_7} →
          {L : Type u_8} →
            [inst_2 : DivisionRing K] →
              [inst_3 : DivisionRing L] →
                {σ : K →+* L} →
                  [inst_4 : Module K E] →
                    [inst_5 : Module L F] → (f : E →ₛₗ.[σ] F) → (x : E) → F → x ∉ f.domain → E →ₛₗ.[σ] F

Extend a LinearPMap to f.domain ⊔ K ∙ x.

Defined in

Mathlib.LinearAlgebra.LinearPMap

Cited by

11 results in Mathlib

Foundations

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

Assumes

AddCommGroupAddCommGroupDivisionRingDivisionRingModuleModule