map_coe_real_complex — Mathlib

English

For any real ℂ-algebra homomorphism f: ℂ →ₐ[ℝ] A and any real x, f(x) = algebraMap ℝ A x.

Русский

Для любого вещественного однородного отображения f: ℂ →ₐ[ℝ] A и любого вещественного числа x выполняется f(x) = algebraMap ℝ A x.

LaTeX

$$$\\\\forall f:\\\\mathbb{C} \\\\to_{\\\\mathbb{R}} A\\\\, (x \\\\in \\\\mathbb{R}) \\\\Rightarrow f(x) =\\\\ algebraMap_{\\\\mathbb{R}} A x$$$

Lean4

/-- We need this lemma since `Complex.coe_algebraMap` diverts the simp-normal form away from
`AlgHom.commutes`. -/
@[simp]
theorem _root_.AlgHom.map_coe_real_complex (f : ℂ →ₐ[ℝ] A) (x : ℝ) : f x = algebraMap ℝ A x :=
  f.commutes x

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