Theorems · Definition · nonassociative algebras

HVertexOperator.coeff

{Γ : Type u_1} →
  [inst : PartialOrder Γ] →
    {R : Type u_2} →
      {V : Type u_3} →
        {W : Type u_4} →
          [inst_1 : CommRing R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : Module R V] →
                [inst_4 : AddCommGroup W] → [inst_5 : Module R W] → HVertexOperator Γ R V W →ₗ[R] Γ → V →ₗ[R] W

The coefficients of a heterogeneous vertex operator, viewed as a linear map to formal power series with coefficients in linear maps.

Defined in

Mathlib.Algebra.Vertex.HVertexOperator

Cited by

12 results in Mathlib

Foundations

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

Assumes

PartialOrderCommRingAddCommGroupModuleAddCommGroupModule