instSMulRealComplex — Mathlib

English

Re(\n r • z) = r • Re(z) for a scalar r ∈ R.

Русский

Re( r • z ) = r • Re(z) для скаляра r ∈ R.

LaTeX

$$$\\operatorname{Re}(r \\cdot z) = r \\cdot \\operatorname{Re}(z)$$$

Lean4

/-- Scalar multiplication by `R` on `ℝ` extends to `ℂ`. This is used here and in
`Mathlib/Data/Complex/Module.lean` to transfer instances from `ℝ` to `ℂ`, but is not
needed outside, so we make it scoped. -/
scoped instance instSMulRealComplex {R : Type*} [SMul R ℝ] : SMul R ℂ where
  smul r x := ⟨r • x.re - 0 * x.im, r • x.im + 0 * x.re⟩

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