algebraMap_injective — Mathlib

English

The algebra map from R to ℍ[R] is injective; distinct scalars remain distinct in the quaternion algebra.

Русский

Отображение алгебраMap из R в ℍ[R] инъективно; разные скаляры сохраняются различными в кватернионной алгебре.

LaTeX

$$$\\operatorname{Injective}\\left(\\mathrm{algebraMap}_R^{\\mathbb{H}(R)}\\right)$$$

Lean4

theorem algebraMap_injective : (algebraMap R ℍ[R] : _ → _).Injective :=
  QuaternionAlgebra.algebraMap_injective

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