invOf_inj

Mathlib.Algebra.Group.Invertible.Defs

URI: https://scilib.ai/kg/mathlib#invOf_inj

English

The inverse operation is injective: if inv(a) = inv(b) then a = b.

Русский

Обратная операция инъективна: если inv(a) = inv(b), то a = b.

LaTeX

$$$\\forall a,b\\, [Invertible\\ a][Invertible\\ b],\\ inv(a) = inv(b) \\Rightarrow a = b$$$

Lean4

@[simp]
theorem invOf_inj [Monoid α] {a b : α} [Invertible a] [Invertible b] : ⅟a = ⅟b ↔ a = b :=
  ⟨invertible_unique _ _, invertible_unique _ _⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru