The presented Weyl algebra and the two-generator identity proved by Stafford’s theorem.

@[reducible, inline]

abbrev Stafford38Challenge.PhaseVar (n : ℕ) : Type

The coordinate and momentum indices in a Weyl algebra of rank n.

Equations

• Stafford38Challenge.PhaseVar n = (Fin n ⊕ Fin n)

def Stafford38Challenge.relation {k : Type u_1} [Field k] {n : ℕ} (omega : Matrix (PhaseVar n) (PhaseVar n) k) (a b : FreeAlgebra k (PhaseVar n)) : Prop

The free-algebra relations prescribing generator commutators from a matrix.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Stafford38Challenge.WeylAlg (k : Type u_1) [Field k] (n : ℕ) : Type u_1

The Weyl algebra presented as the quotient by the standard symplectic commutator relations.

Equations

• Stafford38Challenge.WeylAlg k n = RingQuot (Stafford38Challenge.relation (Matrix.J (Fin n) k))

def Stafford38Challenge.UniversalStatement : Prop

Stafford’s statement that every nonzero d in a characteristic-zero Weyl algebra admits 1 = d * R + F * d * S.

Equations

• One or more equations did not get rendered due to their size.

theorem Stafford38Challenge.universalStatement : UniversalStatement