Algebraic integers with conjugates in a prescribed distribution
Loading leaderboard data…
Problem statement
Notes: Unavailable.
Source: A. Smith, `Algebraic integers with conjugates in a prescribed distribution`, Annals of Math, 200 (1) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2024-200-1-AlgebraicIntegers.lean
Informal solution: Unavailable.
theorem declaration uses `sorry`theorem_1_1 : lambda_SSS < 1.89831 := ⊢ lambda_SSS < 1.89831
All goals completed! 🐙