coe_ofComplex — Mathlib

English

The canonical ℂ → ℍ map coincides with the embedding given by coeComplex, i.e., the algebra hom preserves the standard embedding.

Русский

Каноническое отображение ℂ → ℍ совпадает с вложением, заданным coeComplex; алгебраический гомоморфизм сохраняет стандартное вложение.

LaTeX

$$$\\text{coe_ofComplex}: \\mathbb{C} \\to \\mathbb{H} \\quad = \\quad \\text{coeComplex}.$$$

Lean4

@[simp]
theorem coe_ofComplex : ⇑ofComplex = coeComplex :=
  rfl

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