invOf_neg

Mathlib.Algebra.Ring.Invertible

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

English

In a monoid with distributive negation, if a and -a are invertible, then inv(-a) = -inv(a).

Русский

В моноиде с распределением отрицания, если a и −a обратимы, то inv(−a) = −inv(a).

LaTeX

$$⅟(-a) = -⅟a$$

Lean4

@[simp]
theorem invOf_neg [Monoid R] [HasDistribNeg R] (a : R) [Invertible a] [Invertible (-a)] : ⅟(-a) = -⅟a :=
  invOf_eq_right_inv (by simp)

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

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

Разделы

Аффилиация

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