neg_inv

Mathlib.Algebra.Ring.Basic

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

English

The negation commutes with inversion: −a^{-1} = (−a)^{-1}.

Русский

Отрицание коммутирует с обратной: −a^{-1} = (−a)^{-1}.

LaTeX

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

Lean4

theorem neg_inv : -a⁻¹ = (-a)⁻¹ := by rw [inv_eq_one_div, inv_eq_one_div, div_neg_eq_neg_div]

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

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

Разделы

Аффилиация

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