units_sq

Mathlib.Data.Int.Order.Units

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

English

For any unit u in ℤ, u^2 = 1.

Русский

Для любого элемента-единицы u ∈ ℤ, u^2 = 1.

LaTeX

$$$\forall u \in \mathbb{Z}^{\times}, u^2 = 1.$$$

Lean4

@[simp]
theorem units_sq (u : ℤˣ) : u ^ 2 = 1 := by
  rw [Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one, isUnit_sq u.isUnit]

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

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

Разделы

Аффилиация

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