inv_unique — Mathlib

English

Given a unit equation f y · z = 1, the inverse is uniquely determined by z.

Русский

Если выполнено уравнение, то обратное уникально.

LaTeX

$$$f y \cdot z = 1 \Rightarrow (IsUnit.liftRight (f.restrict S) h y)^{-1} = z$$$

Lean4

/-- Given a MonoidHom `f : M →* N` and Submonoid `S ⊆ M` such that `f(S) ⊆ Nˣ`, for all
`y ∈ S`, `(f y)⁻¹` is unique. -/
@[to_additive /-- Given an AddMonoidHom `f : M →+ N` and Submonoid `S ⊆ M` such that
    `f(S) ⊆ AddUnits N`, for all `y ∈ S`, `- (f y)` is unique. -/
    ]
theorem inv_unique {f : M →* N} (h : ∀ y : S, IsUnit (f y)) {y : S} {z : N} (H : f y * z = 1) :
    (IsUnit.liftRight (f.restrict S) h y)⁻¹ = z :=
  by
  rw [← one_mul _⁻¹, Units.val_mul, mul_inv_left]
  exact H.symm

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