abs_mul — Mathlib

English

The absolute value is multiplicative: |ab| = |a| |b| for any a,b.

Русский

Модуль умножения сохраняется: |ab| = |a| |b|.

LaTeX

$$$|ab| = |a|\,|b|$$$

Lean4

@[simp]
theorem abs_mul (a b : α) : |a * b| = |a| * |b| :=
  by
  rw [abs_eq (mul_nonneg (abs_nonneg a) (abs_nonneg b))]
  rcases le_total a 0 with ha | ha <;> rcases le_total b 0 with hb | hb <;>
    simp only [abs_of_nonpos, abs_of_nonneg, true_or, or_true, neg_mul, mul_neg, neg_neg, *]

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