The universal Stafford 3.8 target

This file owns the exact theorem statement that the end-to-end formalization must eventually prove. It intentionally declares no theorem with an unproved hypothesis and introduces no project axiom.

@[reducible, inline]

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

The presented nth Weyl algebra with its standard symplectic form.

Equations

• Stafford38.WeylAlg k n = Stafford.FreeWeyl k (Fin n ⊕ Fin n) (Matrix.J (Fin n) k)

def Stafford38.UniversalStatement : Prop

Exact proposition required for the publication theorem.

Equations

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