mabs_div_eq_leOnePart_sq — Mathlib

English

In a lattice-ordered commutative group, the division by the absolute part is the inverse square of the negative part: a / |a|ₘ = (a⁻ᵐ²)⁻¹.

Русский

В упорядоченной группе с коммутативным умножением деление на модульную часть равно обратному квадрату от отрицательной части: a / |a|ₘ = (a⁻ᵐ)²)⁻¹.

LaTeX

$$a / |a|ₘ = (a^{-m})^{2} ^{-1}$$

Lean4

@[to_additive abs_sub_eq_two_nsmul_negPart]
theorem mabs_div_eq_leOnePart_sq (a : α) : |a|ₘ / a = a⁻ᵐ ^ 2 := by
  rw [sq, ← mul_div_div_cancel, oneLePart_mul_leOnePart, oneLePart_div_leOnePart]

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