Structures · Algebra

SemilinearMapClass

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

Shape

4 explicit arguments