Theorems · Definition · nonassociative algebras

HVertexOperator

(Γ : Type u_5) →
  [PartialOrder Γ] →
    (R : Type u_6) →
      [inst : CommRing R] →
        (V : Type u_7) →
          (W : Type u_8) →
            [inst_1 : AddCommGroup V] → [Module R V] → [inst_3 : AddCommGroup W] → [Module R W] → Type (max u_7 u_8 u_5)

A heterogeneous Γ-vertex operator over a commutator ring R is an R-linear map from an R-module V to Γ-Hahn series with coefficients in an R-module W.

Defined in

Mathlib.Algebra.Vertex.HVertexOperator

Cited by

16 results in Mathlib

Foundations

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

Assumes

PartialOrderCommRingAddCommGroupModuleAddCommGroupModule