half_sub

Mathlib.Algebra.Field.Basic

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

English

In a division ring with 2 ≠ 0, a/2 − a = −(a/2).

Русский

В делительном кольце при 2 ≠ 0 верно a/2 − a = −(a/2).

LaTeX

$$$\\dfrac{a}{2} - a = -\\left(\\dfrac{a}{2}\\right)$$$

Lean4

theorem half_sub (a : K) : a / 2 - a = -(a / 2) := by rw [← neg_sub, sub_half]

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

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

Разделы

Аффилиация

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