English
The scalar action distributes over addition in ℂ: for any r, x, y in the scalar domain, r · (x + y) = r · x + r · y, and r · 0 = 0.
Русский
Действие скаляра распределено по сложению в ℂ: для любых r, x, y выполняется r · (x + y) = r · x + r · y, и r · 0 = 0.
LaTeX
$$$\\\\forall r \\\\in R, x,y \\\\in \\\\mathbb{C}, (r \\\\cdot (x + y) = r \\\\cdot x + r \\\\cdot y) \\\\wedge (r \\\\cdot 0 = 0)$$$
Lean4
instance (priority := 90) mulAction [Monoid R] [MulAction R ℝ] : MulAction R ℂ
where
one_smul x := by ext <;> simp [smul_re, smul_im, one_smul]
mul_smul r s
x := by
ext <;>
simp [smul_re, smul_im, mul_smul]
-- priority manually adjusted in https://github.com/leanprover-community/mathlib4/pull/11980
