div_eq_inv_self

Mathlib.Algebra.Group.Basic

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

English

In any group G, a / b = b^{-1} is equivalent to a = 1.

Русский

В любой группе G равенство a / b = b^{-1} эквивалентно a = 1.

LaTeX

$$$ a / b = b^{-1} \iff a = 1 $$$

Lean4

@[to_additive (attr := simp)]
theorem div_eq_inv_self : a / b = b⁻¹ ↔ a = 1 := by rw [div_eq_mul_inv, mul_eq_right]

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

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

Разделы

Аффилиация

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