instSMulReal — Mathlib

English

The real scalar action on a Jordan decomposition is defined by a piecewise formula: if r ≥ 0, r acts as r times j; if r < 0, it uses the involutive negation coupled with r's NNReal part.

Русский

Действие действительных чисел на разложение Джордана задано кусочно-постоянно: для r ≥ 0 действует как r умножение, иначе происходит использование обращения с отрицанием.

LaTeX

$$$ r \cdot j = \begin{cases} r \cdot j, & r \ge 0, \\ -((-r)^{+} \cdot j), & r < 0. \end{cases} $$$

Lean4

instance instSMulReal : SMul ℝ (JordanDecomposition α) where
  smul r j := if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)

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