instSMulCommClassOfReal — Mathlib

English

If R and S act on the real numbers with commuting actions, then their actions commute on ℂ as well.

Русский

Если R и S действуют на ℝ с взаимно приводимыми действиями, то их действия коммутируют и на ℂ.

LaTeX

$$$\\\\forall r \\\\in R, \\\\forall s \\\\in S, \\\\forall z \\\\in \\\\mathbb{C}, (r \\\\cdot s) \\\\cdot z = (s \\\\cdot r) \\\\cdot z$$$

Lean4

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

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