one_div_neg_one_eq_neg_one

Mathlib.Algebra.Ring.Basic

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

← MathLib Explorer

English

In a division monoid with a distributive negation, 1 divided by -1 equals -1.

Русский

В делимом моноиде с распределённой операцией отрицания имеет место равенство 1/(−1) = −1.

LaTeX

$$$$ \\frac{1}{-1} = -1. $$$$

Lean4

theorem one_div_neg_one_eq_neg_one : (1 : R) / -1 = -1 :=
  have : -1 * -1 = (1 : R) := by rw [neg_mul_neg, one_mul]
  Eq.symm (eq_one_div_of_mul_eq_one_right this)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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