inv_unique — Mathlib

English

If two units have equal underlying elements, their inverses are equal.

Русский

Если две единицы имеют равные основания, их обращения равны.

LaTeX

$$$\forall u_1,u_2\in \alpha^{\times}:\; u_1 = u_2 \Rightarrow u_1^{-1} = u_2^{-1}$$$

Lean4

@[to_additive]
theorem inv_unique {u₁ u₂ : αˣ} (h : (↑u₁ : α) = ↑u₂) : (↑u₁⁻¹ : α) = ↑u₂⁻¹ :=
  Units.inv_eq_of_mul_eq_one_right <| by rw [h, u₂.mul_inv]

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