instIsCentralScalarOfReal — Mathlib

English

If R acts on ℝ by a MulAction, then this action extends to an action on ℂ by defining r · (a+bi) = (r·a) + (r·b)i.

Русский

Если R действует на ℝ через MulAction, то это действие распространяется на ℂ по формуле r·(a+bi) = (r·a) + (r·b)i.

LaTeX

$$$\\\\forall r \\\\in R, \\\\forall a,b \\\\in \\\\mathbb{R}, \\\\ r \\\\cdot (a + b i) = (r \\\\cdot a) + (r \\\\cdot b) i$$$

Lean4

instance (priority := 90) [SMul R ℝ] [SMul Rᵐᵒᵖ ℝ] [IsCentralScalar R ℝ] : IsCentralScalar R ℂ where
  op_smul_eq_smul r
    x := by
    ext <;>
      simp [smul_re, smul_im, op_smul_eq_smul]
        -- priority manually adjusted in https://github.com/leanprover-community/mathlib4/pull/11980

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