Theorems · Theorem · nonassociative algebras

HVertexOperator.ext

∀ {Γ : 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 B : HVertexOperator Γ R V W), (∀ (v : V), A v = B v) → A = B

Defined in

Mathlib.Algebra.Vertex.HVertexOperator

Cited by

2 results in Mathlib

Foundations

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

Assumes

PartialOrderCommRingAddCommGroupModuleAddCommGroupModule