not_denselyOrdered_withZero_int — Mathlib

English

The multiplicative group with zero built from the integers, denoted by ℤᵐ⁰, is not densely ordered in the given linear order.

Русский

Упорядоченная группа с нулём, порождаемая целыми числами, не имеет плотного порядка.

LaTeX

$$$\\\\neg DenselyOrdered(\\\\mathbb{Z}^\\mathrm{m0})$$$

Lean4

theorem not_denselyOrdered_withZero_int : ¬DenselyOrdered ℤᵐ⁰ :=
  (LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered _).mp ⟨.refl _⟩

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