coe_div — Mathlib

English

Division in the quaternion algebra corresponds to division of the base scalars: the quaternion embedding respects the base-field division.

Русский

Деление в кватернионной алгебре соответствует делению скаляров: вложение базового поля сохраняет деление.

LaTeX

$$$((x / y : R) : \mathbb{H}(R)) = x / y$$$

Lean4

@[norm_cast, simp]
theorem coe_div (x y : R) : ((x / y : R) : ℍ[R]) = x / y :=
  map_div₀ (algebraMap R ℍ[R]) x y

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