Theorems · Inductive type · ring theory

SemilinearMapClass

(F : Type u_14) →
  {R : outParam (Type u_15)} →
    {S : outParam (Type u_16)} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          outParam (R →+* S) →
            (M : outParam (Type u_17)) →
              (M₂ : outParam (Type u_18)) →
                [inst_2 : AddCommMonoid M] →
                  [inst_3 : AddCommMonoid M₂] → [Module R M] → [Module S M₂] → [FunLike F M M₂] → Prop

SemilinearMapClass F σ M M₂ asserts F is a type of bundled σ-semilinear maps M → M₂. See also LinearMapClass F R M M₂ for the case where σ is the identity map on R. A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x.

Defined in

Mathlib.Algebra.Module.LinearMap.Defs

Cited by

16 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

SemiringSemiringAddCommMonoidAddCommMonoidModuleModuleFunLike