Theorems · Definition · linear algebra

LinearPMap.domain

{R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_3} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_4} → [inst_4 : AddCommGroup F] → [inst_5 : Module S F] → (E →ₛₗ.[σ] F) → Submodule R E

The domain of the (semi)linear map.

Defined in

Mathlib.LinearAlgebra.LinearPMap

Cited by

167 results in Mathlib

Foundations

Depth 12 from the axioms, rests on 93 definitions · uses no axioms

Assumes

RingRingAddCommGroupModuleAddCommGroupModule