snd_imJ_dualNumberEquiv_symm — Mathlib

English

Let R be a commutative ring. For any dual-number d ∈ DualNumber(Quaternion R), the snd-coordinate of the imJ-part is preserved under the dual-number symmetry: (dualNumberEquiv.symm d).imJ.snd = d.snd.imJ.

Русский

Пусть R — коммутативное кольцо. Для произвольного двойного числа d над кватернионами R snd-координата imJ-части сохраняется при применении симметрии двойного числа: (dualNumberEquiv.symm d).imJ.snd = d.snd.imJ.

LaTeX

$$$ (dualNumberEquiv.symm d).imJ.snd = d.snd.imJ $$$

Lean4

@[simp]
theorem snd_imJ_dualNumberEquiv_symm (d : DualNumber (Quaternion R)) : (dualNumberEquiv.symm d).imJ.snd = d.snd.imJ :=
  rfl

Похожие утверждения