isUnit_eq_one_or

Mathlib.Algebra.Group.Int.Units

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

English

If u is a unit in the integers, then u equals 1 or u equals -1.

Русский

Если u — единица в целых, то он равен либо 1, либо -1.

LaTeX

$$$ \text{IsUnit}(u) \implies (u = 1 \lor u = -1)$$$

Lean4

theorem isUnit_eq_one_or (hu : IsUnit u) : u = 1 ∨ u = -1 := by simpa only [natAbs_of_isUnit hu] using natAbs_eq u

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

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

Разделы

Аффилиация

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