valMinAbs_zero

Mathlib.Data.ZMod.ValMinAbs

URI: https://scilib.ai/kg/mathlib#ZMod.valMinAbs_zero

← MathLib Explorer

English

For all n, the valMinAbs of the zero element is zero: (0 : ZMod n).valMinAbs = 0.

Русский

Для всех n справедливо (0 : ZMod n).valMinAbs = 0.

LaTeX

$$$\\forall n,\\ (0 : \\mathbb{Z}/n\\mathbb{Z}).valMinAbs = 0$$$

Lean4

@[simp]
theorem valMinAbs_zero : ∀ n, (0 : ZMod n).valMinAbs = 0
  | 0 => by simp only [valMinAbs_def_zero]
  | n + 1 => by simp only [valMinAbs_def_pos, if_true, Int.ofNat_zero, zero_le, val_zero]

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

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

Разделы

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

Аффилиация

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