1096.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/1096
[ErKo98] Erdős, P. and Komornik, V., Developments in non-integer bases. Acta Math. Hungar. (1998), 57--83.
[Fe16] Feng, D.-J., On the topology of polynomials with bounded integer coefficients. J. Eur. Math. Soc. (2016), 181--193.

Imports (1)

theorem Erdos1096.erdos_1096 sorry line 50 source
depends on sorry what this means
Statement uses: Iff, True, Exists, Real, And, GT.gt, OfNat.ofNat, LT.lt, HAdd.hAdd, Nat, StrictMono, Eq, Set, Set.range, Set.ofPred, Finset, Finset.sum, HPow.hPow, Filter.Tendsto, HSub.hSub and 2 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
42 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.