invOf_two_add_invOf_two

Mathlib.Algebra.Ring.Invertible

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

English

If 2 is invertible, then ⅟2 + ⅟2 = 1.

Русский

Если 2 обратимо, то ⅟2 + ⅟2 = 1.

LaTeX

$$⅟2 + ⅟2 = 1$$

Lean4

@[simp]
theorem invOf_two_add_invOf_two [NonAssocSemiring R] [Invertible (2 : R)] : (⅟2 : R) + (⅟2 : R) = 1 := by
  rw [← two_mul, mul_invOf_self]

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

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

Разделы

Аффилиация

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