The left-handed form is the formal-adjoint/opposite-ring image of the written-order Stafford identity.

def Stafford38.LeftHandedCorollary.LeftHandedStatement : Prop

The left-handed Stafford identity 1 = R * d + S * d * F for nonzero Weyl elements.

Equations

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

theorem Stafford38.LeftHandedCorollary.leftHanded_of_universalStatement (h : UniversalStatement) : LeftHandedStatement