Theorems · Definition · functional analysis

WithCStarModule.normedAddCommGroupPiAux

{A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    [inst_1 : PartialOrder A] →
      {ι : Type u_2} →
        {E : ι → Type u_3} →
          [Fintype ι] →
            [inst_3 : (i : ι) → NormedAddCommGroup (E i)] →
              [inst_4 : (i : ι) → Module ℂ (E i)] →
                [inst_5 : (i : ι) → SMul A (E i)] →
                  [(i : ι) → CStarModule A (E i)] →
                    [StarOrderedRing A] → NormedAddCommGroup (WithCStarModule A ((i : ι) → E i))

A normed additive commutative group structure on C⋆ᵐᵒᵈ(A, Π i, E i) with the wrong topology, uniformity and bornology. This is only used to build the instance with the correct forgetful inheritance data.

Defined in

Mathlib.Analysis.CStarAlgebra.Module.Constructions

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonUnitalCStarAlgebraPartialOrderFintypeNormedAddCommGroupModuleSMulCStarModuleStarOrderedRing