Ring commutators

This module contains the multiplication identities used by both the Weyl symplectic layer and the differential-Ore escape layer. The convention is [u,v] = u*v - v*u; no Weyl relation, Ore presentation, or application specific structure is assumed.

def AlgebraicAnalysis.ringCommutator {A : Type u_1} [Ring A] (u v : A) : A

The ring commutator, with the written multiplication order retained.

Equations

• AlgebraicAnalysis.ringCommutator u v = u * v - v * u

@[simp]

theorem AlgebraicAnalysis.ringCommutator_apply {A : Type u_1} [Ring A] (u v : A) : ringCommutator u v = u * v - v * u

theorem AlgebraicAnalysis.ringCommutator_mul {A : Type u_1} [Ring A] (u v x : A) : ringCommutator (u * v) x = u * ringCommutator v x + ringCommutator u x * v

Leibniz expansion in the first argument.

theorem AlgebraicAnalysis.ringCommutator_pow {A : Type u_1} [Ring A] (z x : A) (h : ringCommutator z x = 1) (n : ℕ) : ringCommutator (z ^ n) x = n • z ^ (n - 1)

Iterated commutation with a Weyl-type relation.