Theorems · Inductive type · functional analysis

CStarModule

(A : Type u_1) →
  (E : Type u_2) →
    [inst : NonUnitalSemiring A] →
      [StarRing A] →
        [Module ℂ A] →
          [inst : AddCommGroup E] →
            [Module ℂ E] → [PartialOrder A] → [SMul A E] → [Norm A] → [Norm E] → Type (max u_1 u_2)

A Hilbert C⋆-module is a complex module E endowed with a right A-module structure (where A is typically a C⋆-algebra) and an inner product ⟪x, y⟫_A which satisfies the following properties.

Defined in

Mathlib.Analysis.CStarAlgebra.Module.Defs

Cited by

52 results in Mathlib

Foundations

Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NonUnitalSemiringStarRingModuleAddCommGroupModulePartialOrderSMulNormNorm