instIsScalarTowerOfReal — Mathlib

English

Every scalar from R acting on ℂ via Real scalars is central: r z = z r for all r ∈ R, z ∈ ℂ.

Русский

Каждый скаляр из R, действующий на ℂ через вещественные скаляры, центральен: r z = z r.

LaTeX

$$$\\\\forall r \\\\in R, \\\\forall z \\\\in \\\\mathbb{C}, r \\\\cdot z = z \\\\cdot r$$$

Lean4

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

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