div_mabs_eq_inv_leOnePart_sq — Mathlib

English

In a lattice-ordered commutative group, the division by the positive part yields the inverse square of the negative part: a / |a|ₘ = (a⁻ᵐ)^2)⁻¹.

Русский

Деление на положительную часть даёт обратный квадрат отрицательной части: a / |a|ₘ = (a⁻ᵐ)^2)⁻¹.

LaTeX

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

Lean4

@[to_additive sub_abs_eq_neg_two_nsmul_negPart]
theorem div_mabs_eq_inv_leOnePart_sq (a : α) : a / |a|ₘ = (a⁻ᵐ ^ 2)⁻¹ := by rw [← mabs_div_eq_leOnePart_sq, inv_div]

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