Theorems · Definition · nonassociative algebras

VertexOperator.of_coeff

{R : Type u_1} →
  {V : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module R V] →
          (f : ℤ → Module.End R V) → (∀ (x : V), BddBelow (Function.support fun y => (f y) x)) → VertexOperator R V

Given an endomorphism-valued function on integers satisfying a pointwise bounded-pole condition, we produce a vertex operator.

Defined in

Mathlib.Algebra.Vertex.VertexOperator

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule