eq_one_of_inv_eq' — Mathlib

English

If a⁻¹ = a in a group with order, then a = 1.

Русский

Если элемент равен своему обратному, то он равен единице.

LaTeX

$$$a^{-1} = a \Rightarrow a = 1$$$

Lean4

@[to_additive eq_zero_of_neg_eq]
theorem eq_one_of_inv_eq' (h : a⁻¹ = a) : a = 1 :=
  match lt_trichotomy a 1 with
  | Or.inl h₁ =>
    have : 1 < a := h ▸ one_lt_inv_of_inv h₁
    absurd h₁ this.asymm
  | Or.inr (Or.inl h₁) => h₁
  | Or.inr (Or.inr h₁) =>
    have : a < 1 := h ▸ inv_lt_one'.mpr h₁
    absurd h₁ this.asymm

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