mul_mabs_eq_oneLePart_sq — Mathlib

English

In a lattice-ordered commutative group, the product a · |a|ₘ equals the square of the positive part: a · |a|ₘ = (a⁺ᵐ)².

Русский

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

LaTeX

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

Lean4

@[to_additive add_abs_eq_two_nsmul_posPart]
theorem mul_mabs_eq_oneLePart_sq (a : α) : a * |a|ₘ = a⁺ᵐ ^ 2 := by rw [mul_comm, mabs_mul_eq_oneLePart_sq]

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