one_sub_invOf_two

Mathlib.Algebra.Ring.Invertible

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

← MathLib Explorer

English

If 2 is invertible in a ring, then 1 − ⅟2 = ⅟2.

Русский

Если 2 обратимо в кольце, то 1 − ⅟2 = ⅟2.

LaTeX

$$1 - ⅟2 = ⅟2$$

Lean4

@[simp]
theorem one_sub_invOf_two [Ring R] [Invertible (2 : R)] : 1 - (⅟2 : R) = ⅟2 :=
  (isUnit_of_invertible (2 : R)).mul_right_inj.1 <| by
    rw [mul_sub, mul_invOf_self, mul_one, ← one_add_one_eq_two, add_sub_cancel_right]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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