coe_algebraMap — Mathlib

English

The algebra map from R into the quaternion algebra H(R,c1,c2,c3) agrees with the canonical embedding; equivalently, the algebra map sends each r ∈ R to its image ↑r in H.

Русский

Алгебраическая карта из R в H(R,c1,c2,c3) совпадает с каноническим вложением; то есть каждый r ∈ R отображается как ↑r.

LaTeX

$$$(\operatorname{algebraMap}_R^{\mathbb{H}})(r) = \uparrow r$$$

Lean4

@[norm_cast, simp]
theorem coe_algebraMap : ⇑(algebraMap R ℍ[R,c₁,c₂,c₃]) = coe :=
  rfl

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