Real cyclotomic integer with house at most 2
cyclotomic_integer_house_le_two
Submitter: Kim Morrison.
Notes: The <= 2 branch of Theorem 1.0.5 from Calegari--Morrison--Snyder, stated using Mathlib's NumberField.house.
Source: https://arxiv.org/pdf/1004.0665
Informal solution: If the house is at most 2, then it equals 2 cos(pi / m) for some positive integer m.
theorem declaration uses `sorry`cyclotomic_integer_house_le_two {K : Type*} [Field K] [NumberField K] [Algebra ℚ K]
(n : ℕ) [NeZero n] [IsCyclotomicExtension {n} ℚ K] {β : K}
(hβ_int : IsIntegral ℤ β)
(hβ_real : β ∈ NumberField.maximalRealSubfield K) :
house β ≤ 2 →
house β = 2 ∨ ∃ m : ℕ, 0 < m ∧ house β = 2 * Real.cos (Real.pi / m) := K:Type u_1inst✝⁴:Field Kinst✝³:NumberField Kinst✝²:Algebra ℚ Kn:ℕinst✝¹:NeZero ninst✝:IsCyclotomicExtension {n} ℚ Kβ:Khβ_int:IsIntegral ℤ βhβ_real:β ∈ maximalRealSubfield K⊢ house β ≤ 2 → house β = 2 ∨ ∃ m, 0 < m ∧ house β = 2 * Real.cos (Real.pi / ↑m)
All goals completed! 🐙Solved by
Not yet solved.