isUnit_sq

Mathlib.Data.Int.Order.Units

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

English

If a is a unit in ℤ, then a^2 = 1.

Русский

Если a является единицей в ℤ, то a^2 = 1.

LaTeX

$$$\forall a \in \mathbb{Z}, \mathrm{IsUnit}(a) \Rightarrow a^2 = 1.$$$

Lean4

theorem isUnit_sq {a : ℤ} (ha : IsUnit a) : a ^ 2 = 1 := by rw [sq, isUnit_mul_self ha]

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

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

Разделы

Аффилиация

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