mabs_mul_eq_oneLePart_sq — Mathlib

English

In a lattice-ordered commutative group, the absolute value part interacts with the element via a square: |a|ₘ · a = (a⁺ᵐ)².

Русский

В упорядоченной группе с коммутативным умножением положительная часть связана с элементом через квадрат: |a|ₘ · a = (a⁺ᵐ)².

LaTeX

$$|a|ₘ \cdot a = (a^{+m})^{2}$$

Lean4

@[to_additive abs_add_eq_two_nsmul_posPart]
theorem mabs_mul_eq_oneLePart_sq (a : α) : |a|ₘ * a = a⁺ᵐ ^ 2 := by
  rw [sq, ← mul_mul_div_cancel a⁺ᵐ, oneLePart_mul_leOnePart, oneLePart_div_leOnePart]

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