algebraMap_def — Mathlib

English

The canonical algebra homomorphism from R into the quaternion algebra ℍ[R] coincides with the usual inclusion, i.e., algebraMap_Rℍ equals the coercion map.

Русский

Канонический алгебраический гомоморфизм из R в кватернионную алгебру ℍ[R] совпадает с обычным включением; то есть algebraMap = coe.

LaTeX

$$$\mathrm{algebraMap}: R \to \mathbb{H}[R] = \mathrm{coe}$$$

Lean4

@[simp]
theorem algebraMap_def : ⇑(algebraMap R ℍ[R]) = coe :=
  rfl

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