map_units_int

Mathlib.Data.Int.AbsoluteValue

URI: https://scilib.ai/kg/mathlib#AbsoluteValue.map_units_int

English

The absolute value of any unit of the integers is 1.

Русский

Абсолютная величина любого элемента из единиц целого равна 1.

LaTeX

$$$$ \\lvert x \\rvert = 1 \\quad \\text{for } x \\in \\mathbb{Z}^\\times $$$$

Lean4

@[simp]
theorem map_units_int (abv : AbsoluteValue ℤ S) (x : ℤˣ) : abv x = 1 := by
  rcases Int.units_eq_one_or x with (rfl | rfl) <;> simp

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

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

Разделы

Аффилиация

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