coe_smul — Mathlib

English

For every real x and every y in E, the action of x viewed as a complex scalar coincides with the real scalar action: (x : ℂ) • y = x • y.

Русский

Для каждого действительного числа x и элемента y в E вероятность действия x как скаляра ℂ совпадает с действием x как скаляра ℝ: (x : ℂ) • y = x • y.

LaTeX

$$$ \forall x \in \mathbb{R}, \forall y \in E:\ (x : \mathbb{C}) \cdot y = x \cdot y. $$$

Lean4

@[simp, norm_cast]
theorem coe_smul {E : Type*} [AddCommGroup E] [Module ℂ E] (x : ℝ) (y : E) : (x : ℂ) • y = x • y :=
  rfl

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