abs_smul — Mathlib

English

For a ring R acting on a lattice-ordered module M, the absolute value respects the scalar action: |a · b| = |a| · |b|.

Русский

Для кольца R, действующего на модуль M с упорядочением, выполняется |a·b| = |a|·|b|.

LaTeX

$$$\\lvert a \\cdot b \\rvert = \\lvert a \\rvert \\cdot \\lvert b \\rvert.$$$

Lean4

@[simp]
theorem abs_smul (a : R) (b : M) : |a • b| = |a| • |b| := by
  obtain ha | ha := le_total a 0 <;> obtain hb | hb := le_total b 0 <;>
    simp [*, abs_of_nonneg, abs_of_nonpos, smul_nonneg, smul_nonpos_of_nonneg_of_nonpos,
      smul_nonpos_of_nonpos_of_nonneg, smul_nonneg_of_nonpos_of_nonpos]

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