coe_sub

Mathlib.Algebra.Quaternion

URI: https://scilib.ai/kg/mathlib#Quaternion.coe_sub

English

The embedding preserves subtraction: ((x - y) : R) → ℍ[R] equals x - y in ℍ[R].

Русский

Встраивание сохраняет вычитание: ((x - y) : R) → ℍ[R] равняется x - y в ℍ[R].

LaTeX

$$$ ((x - y : R) : \\mathbb{H}(R)) = x - y $$$

Lean4

@[simp, norm_cast]
theorem coe_sub : ((x - y : R) : ℍ[R]) = x - y :=
  QuaternionAlgebra.coe_sub x y

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru