coe_zsmul — Mathlib

English

Integer scalar multiplication is preserved by the embedding: (↑(n • x) : EReal) = n • (x : EReal).

Русский

Целочисленное умножение сохраняется внутри встраивания: ↑(n·x) = n·(↑x).

LaTeX

$$$$ (↑(n \cdot x) : \mathrm{EReal}) = n \cdot (x : \mathrm{EReal}) $$$$

Lean4

@[norm_cast]
theorem coe_zsmul (n : ℤ) (x : ℝ) : (↑(n • x) : EReal) = n • (x : EReal) :=
  map_zsmul' (⟨⟨(↑), coe_zero⟩, coe_add⟩ : ℝ →+ EReal) coe_neg _ _

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