Structures · Analysis

SemilinearIsometryClass

SemilinearIsometryClass F σ E E₂ asserts F is a type of bundled σ-semilinear isometries E → E₂. See also LinearIsometryClass F R E E₂ 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.Analysis.Normed.Operator.LinearIsometry

Shape

4 explicit arguments · adds norm_map