toNNRat_mul — Mathlib

English

If p ≥ 0, then toNNRat(p · q) = toNNRat(p) · toNNRat(q).

Русский

Если p ≥ 0, то toNNRat(p·q) = toNNRat(p)·toNNRat(q).

LaTeX

$$$\text{If } p \ge 0:\quad \operatorname{toNNRat}(p \cdot q) = \operatorname{toNNRat}(p) \cdot \operatorname{toNNRat}(q).$$$

Lean4

theorem toNNRat_mul (hp : 0 ≤ p) : toNNRat (p * q) = toNNRat p * toNNRat q :=
  by
  rcases le_total 0 q with hq | hq
  · ext; simp [toNNRat, hp, hq, mul_nonneg]
  · have hpq := mul_nonpos_of_nonneg_of_nonpos hp hq
    rw [toNNRat_eq_zero.2 hq, toNNRat_eq_zero.2 hpq, mul_zero]

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