coe_sub — Mathlib

English

The embedding respects subtraction: ((x - y) : R) maps to the difference of the embeddings: ((x - y) : ℍ) = (x : ℍ) - (y : ℍ).

Русский

Вложение сохраняет вычитание: ((x - y) : R) отображается как разность вложений: ((x - y) : ℍ) = (x : ℍ) - (y : ℍ).

LaTeX

$$$((x - y) : \mathbb{H}(R;c_1,c_2,c_3)) = (x : \mathbb{H}(R;c_1,c_2,c_3)) - (y : \mathbb{H}(R;c_1,c_2,c_3)).$$$

Lean4

@[norm_cast, simp]
theorem coe_sub : ((x - y : R) : ℍ[R,c₁,c₂,c₃]) = x - y :=
  (algebraMap R ℍ[R,c₁,c₂,c₃]).map_sub x y

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