Theorems · Inductive type · linear algebra

LinearPMap

{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] →
              [Module R E] → (F : Type u_4) → [inst : AddCommGroup F] → [Module S F] → Type (max u_3 u_4)

A LinearPMap σ E F or E →ₛₗ.[σ] F is a (semi)linear map from a submodule of E to F.

Defined in

Mathlib.LinearAlgebra.LinearPMap

Cited by

179 results in Mathlib

Foundations

Depth 11 from the axioms, rests on 91 definitions · uses no axioms

Assumes

RingRingAddCommGroupModuleAddCommGroupModule