abs_eq_normalize

Mathlib.Algebra.GCDMonoid.Nat

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

← MathLib Explorer

English

For any integer z, |z| equals the normalization of z.

Русский

Для любого целого z выполнено: |z| = normalize(z).

LaTeX

$$$$|z| = \operatorname{normalize}(z)$$$$

Lean4

theorem abs_eq_normalize (z : ℤ) : |z| = normalize z := by
  cases le_total 0 z <;> simp [abs_of_nonneg, abs_of_nonpos, normalize_of_nonneg, normalize_of_nonpos, *]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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