Mathlib Map

Structures · Analysis

CStarModule

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
Shape
2 explicit arguments · adds inner_add_right, inner_self_nonneg, inner_self, inner_op_smul_right, inner_smul_right_complex, star_inner, norm_eq_sqrt_norm_inner_self

Extends1

Extended by0

Nothing extends this class yet.

Concrete types that are instances1

  • Complex

How is a type an instance?

Loading the hierarchy index…

Assumed by65

Ancestors1