Theorems · Definition · ring theory

LinearMapClass

(F : Type u_14) →
  (R : outParam (Type u_15)) →
    (M : Type u_16) →
      (M₂ : Type u_17) →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M₂] → [Module R M] → [Module R M₂] → [FunLike F M M₂] → Prop

LinearMapClass F R M M₂ asserts F is a type of bundled R-linear maps M → M₂. This is an abbreviation for SemilinearMapClass F (RingHom.id R) M M₂.

Defined in

Mathlib.Algebra.Module.LinearMap.Defs

Cited by

25 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms

Assumes

SemiringAddCommMonoidAddCommMonoidModuleModuleFunLike