denseRange_zsmul_iff — Mathlib

English

The addition-range of the integer multiples in AddCircle(p) is dense if and only if addOrderOf a is infinite.

Русский

Плотность диапазона Z-множителей в AddCircle(p) эквивалентна бесконечному порядку элемента a.

LaTeX

$$$$ \\text{DenseRange}(\\cdot \\;\\text{on } a) \\iff addOrderOf(a) = 0. $$$$

Lean4

/-- The multiples of a number `a` are dense on a circle of length `p > 0`
iff `a` has infinite additive order. -/
theorem denseRange_zsmul_iff {p : ℝ} [Fact (0 < p)] {a : AddCircle p} :
    DenseRange (· • a : ℤ → AddCircle p) ↔ addOrderOf a = 0 :=
  by
  rcases QuotientAddGroup.mk_surjective a with ⟨a, rfl⟩
  simp [denseRange_zsmul_coe_iff, isOfFinAddOrder_iff_exists_rat_eq_div, Irrational]

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