instModule — Mathlib

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

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