oneLePart_mul_leOnePart — Mathlib

English

For any a in a lattice-ordered group, the product of the positive and the negative part equals the multiplicative absolute value: a⁺ᵐ · a⁻ᵐ = |a|ₘ.

Русский

Для любого a выполняется a⁺ᵐ · a⁻ᵐ = |a|ₘ.

LaTeX

$$a^{+m} \cdot a^{-m} = |a|_{m}$$

Lean4

@[to_additive]
theorem oneLePart_mul_leOnePart (a : α) : a⁺ᵐ * a⁻ᵐ = |a|ₘ :=
  by
  rw [oneLePart_def, sup_mul, one_mul, leOnePart_def, mul_sup, mul_one, mul_inv_cancel, sup_assoc, ← sup_assoc a,
    sup_eq_right.2 le_sup_right]
  exact sup_eq_left.2 <| one_le_mabs a

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