isUnit_eq_or_eq_neg

Mathlib.Algebra.Group.Int.Units

URI: https://scilib.ai/kg/mathlib#Int.isUnit_eq_or_eq_neg

English

For units u and v, either u = v or u = -v.

Русский

Для единиц u и v верно либо u = v, либо u = -v.

LaTeX

$$$ u = v \;\lor\; u = -v $$$

Lean4

theorem isUnit_eq_or_eq_neg (hu : IsUnit u) (hv : IsUnit v) : u = v ∨ u = -v :=
  or_iff_not_imp_left.2 (isUnit_ne_iff_eq_neg hu hv).1

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

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

Разделы

Аффилиация

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