leOnePart_inv — Mathlib

English

In a lattice-ordered group, a⁻ᵐ equals the inverse constrained by the min of a and 1: a⁻ᵐ = inv(min(a,1)).

Русский

В решёточно упорядоченной группе a⁻ᵐ равно обратному элементу, ограниченному минимумом a и 1: a⁻ᵐ = inv(min(a,1)).

LaTeX

$$$a^{-m} = (\min\{a,1\})^{-1}$$$

Lean4

@[to_additive (attr := simp)]
theorem leOnePart_inv (a : α) : a⁻¹⁻ᵐ = a⁺ᵐ := by simp [oneLePart, leOnePart]

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