neg_div'

Mathlib.Algebra.Ring.Basic

URI: https://scilib.ai/kg/mathlib#neg_div'

English

The equality -(b/a) = (-b)/a holds, i.e., negating a quotient equals quotient with negated numerator.

Русский

Равенство −(b/a) = (−b)/a: отрицание числителя можно вынести за знак деления.

LaTeX

$$$$ -\\left(\\frac{b}{a}\\right) = \\frac{-b}{a}. $$$$

Lean4

theorem neg_div' (a b : R) : -(b / a) = -b / a := by simp [neg_div]

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

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

Разделы

Аффилиация

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