Theorems · Theorem · nonassociative algebras

HVertexOperator.coeff_apply_apply

∀ {Γ : 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]
  (A : HVertexOperator Γ R V W) (n : Γ) (v : V), (HVertexOperator.coeff A n) v = ((HahnModule.of R).symm (A v)).coeff n

Defined in

Mathlib.Algebra.Vertex.HVertexOperator

Cited by

3 results in Mathlib

Foundations

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

Assumes

PartialOrderCommRingAddCommGroupModuleAddCommGroupModule