complexToReal — Mathlib

English

Let A be a semiring with a ℂ-algebra structure. Then A inherits an ℝ-algebra structure via restriction of scalars.

Русский

Пусть A — полугруппа с структурой ℂ-алгебры. Тогда A наследует структуру ℝ-алгебры через ограничение скаляров.

LaTeX

$$$ (\\\\forall A)\\; (\\\\text{Semiring}(A) \\wedge \\\\text{Algebra}_{\\\\mathbb{C}}(A)) \Rightarrow \\\\text{Algebra}_{\\\\mathbb{R}}(A). $$$

Lean4

instance (priority := 900) complexToReal {A : Type*} [Semiring A] [Algebra ℂ A] : Algebra ℝ A :=
  RestrictScalars.algebra ℝ ℂ A

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