sub_half

Mathlib.Algebra.Field.Basic

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

English

In a division ring with 2 ≠ 0, a − a/2 = a/2 for all a.

Русский

В делительном кольце при условии 2 ≠ 0 выполняется a − a/2 = a/2 для каждого a.

LaTeX

$$$a - \\dfrac{a}{2} = \\dfrac{a}{2}, \\quad 2 \\neq 0$$$

Lean4

theorem sub_half (a : K) : a - a / 2 = a / 2 := by rw [sub_eq_iff_eq_add, add_halves]

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

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

Разделы

Аффилиация

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