ofComplex — Mathlib

English

There is an ℝ-algebra homomorphism from ℂ to ℍ given by z ↦ (z.re) + (z.im) i, i.e., z maps to a quaternion with real and i-components only.

Русский

Существует ℝ-алгебраомоморфизм ℂ в ℍ, заданный z ↦ (z.re) + (z.im) i, то есть z отправляется в кватернион с действительной и мнимой по оси i компонентами.

LaTeX

$$$\\text{OfComplex}: \\mathbb{C} \\to \\mathbb{H},\\; z \\mapsto \\hat{z} = (\\Re z) + (\\Im z) i.$$$

Lean4

/-- Coercion `ℂ →ₐ[ℝ] ℍ` as an algebra homomorphism. -/
def ofComplex : ℂ →ₐ[ℝ] ℍ where
  toFun := (↑)
  map_one' := rfl
  map_zero' := rfl
  map_add' := coeComplex_add
  map_mul' := coeComplex_mul
  commutes' _ := rfl

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