diff --git a/LeanEval/NumberTheory/SmallHouse.lean b/LeanEval/NumberTheory/SmallHouse.lean
index 9d15dba..cfa32fb 100644
--- a/LeanEval/NumberTheory/SmallHouse.lean
+++ b/LeanEval/NumberTheory/SmallHouse.lean
@@ -32,7 +32,7 @@ theorem cyclotomic_integer_house_between_two_and_76_33
     (hβ_int : IsIntegral ℤ β)
     (hβ_real : β ∈ NumberField.maximalRealSubfield K) :
     (2 < house β ∧ house β < (76 : ℝ) / 33) →
-      house β = (7 + Real.sqrt 3) / 2 ∨
+      house β = (Real.sqrt 7 + Real.sqrt 3) / 2 ∨
       house β = Real.sqrt 5 ∨
       house β = 1 + 2 * Real.cos (2 * Real.pi / 7) ∨
       house β = (1 + Real.sqrt 5) / Real.sqrt 2 ∨