snd_imK_dualNumberEquiv_symm — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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