smul_negPart — Mathlib

English

Scaling a Jordan decomposition by a nonnegative real scales its negative part similarly.

Русский

Умножение разложения Джордана на неотрицательное вещественное число масштабирует его отрицательную часть аналогично.

LaTeX

$$$ (r \cdot j).\mathrm{negPart} = r \cdot j.\mathrm{negPart} \quad (r \in \mathbb{N}\mathbb{N})$$$

Lean4

@[simp]
theorem smul_negPart (r : ℝ≥0) : (r • j).negPart = r • j.negPart :=
  rfl

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