invOf_eq_inv

Mathlib.Algebra.GroupWithZero.Invertible

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

English

In a GroupWithZero, for invertible a, invOf(a) equals the multiplicative inverse a^{-1}.

Русский

В группе с нулём, для обращаемого a, invOf(a) равно обратному элементу a^{-1}.

LaTeX

$$$a \\\\text{ invertible} \\\Rightarrow \\\\operatorname{invOf}(a) = a^{-1}$$$

Lean4

@[simp]
theorem invOf_eq_inv (a : α) [Invertible a] : ⅟a = a⁻¹ :=
  invOf_eq_right_inv (mul_inv_cancel₀ (Invertible.ne_zero a))

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

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

Разделы

Аффилиация

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