add_self_div_two

Mathlib.Algebra.Field.Basic

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

English

If 2 is nonzero in K, then (a + a)/2 = a.

Русский

Если 2 ≠ 0 в K, то (a + a)/2 = a.

LaTeX

$$$$\frac{a+a}{2} = a \quad(2\neq 0).$$$$

Lean4

@[simp]
theorem add_self_div_two (a : K) : (a + a) / 2 = a := by rw [← mul_two, mul_div_cancel_right₀ a two_ne_zero]

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

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

Разделы

Аффилиация

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