leOnePart_mul_oneLePart — Mathlib

English

The product in the opposite order also equals the multiplicative absolute value: a⁻ᵐ · a⁺ᵐ = |a|ₘ.

Русский

Произведение в обратном порядке также дает модуль: a⁻ᵐ · a⁺ᵐ = |a|ₘ.

LaTeX

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

Lean4

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

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