Structures · Topology

ContinuousSemilinearMapClass

ContinuousSemilinearMapClass F σ M M₂ asserts F is a type of bundled continuous σ-semilinear maps M → M₂. See also ContinuousLinearMapClass 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.Topology.Algebra.Module.ContinuousLinearMap.Basic

Shape

4 explicit arguments