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