English
The action of R on Real extends to an action on ℂ: r • z is defined so that scalar multiplication respects addition and scalar distributivity.
Русский
Действие R на Real распространяется на ℂ: отношение r • z определяется так, чтобы сохранялись сложение и распределимость скаляра.
LaTeX
$$$\\\\forall r \\\\in R, \\\\forall x,y \\\\in \\\\mathbb{C}, \\\\ (r \\\\cdot (x + y) = r \\\\cdot x + r \\\\cdot y) \\\\wedge \\\\ (r \\\\cdot 0 = 0)$$$
Lean4
instance (priority := 90) distribSMul [DistribSMul R ℝ] : DistribSMul R ℂ
where
smul_add r x y := by ext <;> simp [smul_re, smul_im, smul_add]
smul_zero
r := by
ext <;>
simp [smul_re, smul_im, smul_zero]
-- priority manually adjusted in https://github.com/leanprover-community/mathlib4/pull/11980
