smul_posPart — Mathlib

English

Scaling a Jordan decomposition by a nonnegative real properly scales its positive part.

Русский

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

LaTeX

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

Lean4

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

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