zero_eq_inv

Mathlib.Algebra.GroupWithZero.Basic

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

English

In a group with zero, 0 = a^{-1} if and only if 0 = a.

Русский

В группе с нулём, 0 = a^{-1} тогда и только тогда, когда 0 = a.

LaTeX

$$$0 = a^{-1} \\\\iff 0 = a$$$

Lean4

@[simp]
theorem zero_eq_inv {a : G₀} : 0 = a⁻¹ ↔ 0 = a :=
  eq_comm.trans <| inv_eq_zero.trans eq_comm

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

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

Разделы

Аффилиация

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