coe_add — Mathlib

English

Let R be a ring and ℍ[R,c1,c2,c3] the corresponding quaternion algebra. The natural inclusion ι: R → ℍ[R,c1,c2,c3] preserves addition; for all x,y ∈ R, ι(x+y) = ι(x) + ι(y).

Русский

Пусть R — кольцо и ℍ[R,c1,c2,c3] — соответствующая алгебра Куaternion. Естественное вложение ι: R → ℍ сохраняет сложение: для любых x,y ∈ R выполняется ι(x+y) = ι(x) + ι(y).

LaTeX

$$$\operatorname{coe}(x+y) = \operatorname{coe}(x) + \operatorname{coe}(y)$$$

Lean4

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

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