coe_neg

Mathlib.Algebra.Quaternion

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

English

The embedding from the base ring commutes with negation: (-x in R) maps to -x in the quaternion algebra, i.e., ((-x) : ℍ[R]) = -x.

Русский

Встраивание из базового кольца сохраняет отрицание: ((-x) : ℍ[R]) = -x.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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