English
There is an ℝ-algebra structure on ℂ induced by the real numbers via the real embedding.
Русский
Для ℂ существует структура ℝ-алгебры, индуцированная через действительное вложение.
LaTeX
$$$\\\\text{Algebra } R \\\\mathbb{C}$$$
Lean4
instance (priority := 100) instModule [Semiring R] [Module R ℝ] : Module R ℂ
where
add_smul r s x := by ext <;> simp [smul_re, smul_im, add_smul]
zero_smul
r := by
ext <;>
simp [smul_re, smul_im, zero_smul]
-- priority manually adjusted in https://github.com/leanprover-community/mathlib4/pull/11980