add_halves

Mathlib.Algebra.Field.Basic

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

English

For any a in K, a/2 + a/2 = a.

Русский

Для любого a в K, a/2 + a/2 = a.

LaTeX

$$$$\frac{a}{2} + \frac{a}{2} = a.$$$$

Lean4

@[simp]
theorem add_halves (a : K) : a / 2 + a / 2 = a := by rw [← add_div, add_self_div_two]

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

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

Разделы

Аффилиация

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