sub_eq_add

Mathlib.Algebra.CharP.Two

URI: https://scilib.ai/kg/mathlib#CharTwo.sub_eq_add

English

In characteristic 2, subtraction equals addition: x − y = x + y.

Русский

В характеристике 2 вычитание эквивалентно сложению: x − y = x + y.

LaTeX

$$$x - y = x + y$$$

Lean4

@[scoped simp]
theorem sub_eq_add (x y : R) : x - y = x + y := by rw [sub_eq_add_neg, neg_eq]

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

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

Разделы

Аффилиация

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