instDistribMulActionOfReal — Mathlib

English

If R is a semiring and E is a real module with an R-action, then ℂ inherits an R-module structure extending the real action.

Русский

Если R — полукольцо и E — вещественный модуль с действием R, тогда ℂ наследует структуру R-модуля, расширяющую вещественное действие.

LaTeX

$$$\\\\forall R \\\\text{ } E \\\\text{ with } [\\\\text{Module } R \\\\mathbb{R} E] \\\\Rightarrow \\\\text{Module } R \\\\mathbb{C} E$$$

Lean4

instance (priority := 90) [Semiring R] [DistribMulAction R ℝ] : DistribMulAction R ℂ :=
  { Complex.distribSMul, Complex.mulAction with }
    -- priority manually adjusted in https://github.com/leanprover-community/mathlib4/pull/11980

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