isUnit — Mathlib

English

Let G be a group. Then every element a ∈ G has a multiplicative inverse a^{-1} ∈ G, so a is a unit: there exists b ∈ G with a b = b a = 1.

Русский

Пусть G — группа. Тогда каждый элемент a ∈ G обратим, то есть существует b ∈ G такое, что a b = b a = 1.

LaTeX

$$$\\forall a \\in G, \\exists b \\in G: a b = 1 \\land b a = 1$$$

Lean4

@[to_additive]
theorem isUnit [Group α] (a : α) : IsUnit a :=
  ⟨⟨a, a⁻¹, mul_inv_cancel _, inv_mul_cancel _⟩, rfl⟩
    -- namespace

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