Formal target: Corpus.BooksBugeaudDistributionModuloOneProblem106.problem_10_6_variant_1

Problem 10.6.

Exact formal statement

Exists.{1} fun m =>
  And (StrictMono.{0, 0} m)
    (And (Corpus.BooksBugeaudDistributionModuloOneProblem106.IsGenuinelySublacunary m)
      (∀ (ξ : Real),
        Irrational ξ →
          Dense.{0} (Set.range.{0, 1} fun n => QuotientAddGroup.mk.{0} (HMul.hMul.{0, 0, 0} ξ (Nat.cast.{0} (m n))))))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record