leanprover-community · Ruben-VandeVelde · Aug 20, 2020 · Aug 5, 2022 · Aug 6, 2022 · Aug 6, 2022
diff --git a/src/analysis/transcendental/basic.lean b/src/analysis/transcendental/basic.lean
@@ -0,0 +1,6 @@
+import data.real.basic
+import ring_theory.localization.integral
+
+theorem transcendental_iff_transcendental_over_ℚ (x : ℝ) :
+  transcendental ℤ x ↔ transcendental ℚ x :=
+iff.not $ is_fraction_ring.is_algebraic_iff ℤ ℚ ℝ
-iff.not $ is_fraction_ring.is_algebraic_iff ℤ ℚ ℝ
+(is_fraction_ring.is_algebraic_iff ℤ ℚ ℝ).not
-iff.not $ is_fraction_ring.is_algebraic_iff ℤ ℚ ℝ
+(is_fraction_ring.is_algebraic_iff ℤ ℚ ℝ).not
diff --git a/src/analysis/transcendental/e_transcendental.lean b/src/analysis/transcendental/e_transcendental.lean