inv_mk — Mathlib

English

In the valued group with zero structure, for x ∈ R, y a positive submonoid element, and hx ≠ x ≤ᵥ 0, the inverse of the constructed element mk x y is mk (y : R) ⟨x, hx⟩.

Русский

В целочисленной группе значений с нулём, для x ∈ R, y ∈ posSubmonoid R и hx : ¬ x ≤ᵥ 0, обратный элемент к mk x y равен mk (y : R) ⟨x, hx⟩.

LaTeX

$$$ (ValueGroupWithZero.mk x y)^{-1} = ValueGroupWithZero.mk (y : R) \langle x, hx \rangle $$$

Lean4

@[simp]
theorem inv_mk (x : R) (y : posSubmonoid R) (hx : ¬x ≤ᵥ 0) :
    (ValueGroupWithZero.mk x y)⁻¹ = ValueGroupWithZero.mk (y : R) ⟨x, hx⟩ :=
  dif_neg hx

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