Theorems · Inductive type · functional analysis

SemilinearIsometryClass

(𝓕 : Type u_11) →
  {R : outParam (Type u_12)} →
    {R₂ : outParam (Type u_13)} →
      [inst : Semiring R] →
        [inst_1 : Semiring R₂] →
          outParam (R →+* R₂) →
            (E : outParam (Type u_14)) →
              (E₂ : outParam (Type u_15)) →
                [inst_2 : SeminormedAddCommGroup E] →
                  [inst_3 : SeminormedAddCommGroup E₂] → [Module R E] → [Module R₂ E₂] → [FunLike 𝓕 E E₂] → Prop

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

Cited by

11 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

SemiringSemiringSeminormedAddCommGroupSeminormedAddCommGroupModuleModuleFunLike