inv_neg

Mathlib.Algebra.Ring.Basic

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

English

The inverse of a negated element is the negation of the inverse: (-a)^{-1} = -(a^{-1}).

Русский

Обратное к −a равно −(a^{-1}).

LaTeX

$$$$ (-a)^{-1} = -(a^{-1}). $$$$

Lean4

@[simp]
theorem inv_neg : (-a)⁻¹ = -a⁻¹ := by rw [neg_inv]

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

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

Разделы

Аффилиация

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