coe_neg

Mathlib.Algebra.Quaternion

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

English

Let ι: R → ℍ[R,c1,c2,c3] be the inclusion. The embedding respects negation: ι(-x) = -ι(x) for all x ∈ R.

Русский

Пусть ι: R → ℍ[...]. Встраивание сохраняет отрицание: ι(-x) = -ι(x) для всякого x ∈ R.

LaTeX

$$$\operatorname{coe}(-x) = -\operatorname{coe}(x)$$$

Lean4

@[simp, norm_cast]
theorem coe_neg : ((-x : R) : ℍ[R,c₁,c₂,c₃]) = -x := by ext <;> simp

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

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

Разделы

Аффилиация

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