feat(ring_theory/algebraic data/real/irrational): add a proof that a …

…transcendental real number is irrational (#6721)


Zulip:
https://leanprover.zulipchat.com/#narrow/stream/263328-triage

src/data/real/irrational.lean

@@ -9,6 +9,7 @@ import ring_theory.int.basic
 import data.polynomial.eval
 import data.polynomial.degree
 import tactic.interval_cases
+import ring_theory.algebraic
 /-!
 # Irrational real numbers
 
@@ -28,6 +29,11 @@ lemma irrational_iff_ne_rational (x : ℝ) : irrational x ↔ ∀ a b : ℤ, x 
 by simp only [irrational, rat.forall, cast_mk, not_exists, set.mem_range, cast_coe_int, cast_div,
   eq_comm]
 
+/-- A transcendental real number is irrational. -/
+lemma transcendental.irrational {r : ℝ} (tr : transcendental ℚ r) :
+  irrational r :=
+by { rintro ⟨a, rfl⟩, exact tr (is_algebraic_algebra_map a) }
+
 /-!
 ### Irrationality of roots of integer and rational numbers
 -/

src/ring_theory/algebraic.lean

@@ -74,6 +74,12 @@ variables (R : Type u) {A : Type v} [comm_ring R] [nontrivial R] [ring A] [algeb
 lemma is_integral.is_algebraic {x : A} (h : is_integral R x) : is_algebraic R x :=
 by { rcases h with ⟨p, hp, hpx⟩, exact ⟨p, hp.ne_zero, hpx⟩ }
 
+variables {R}
+
+/-- An element of `R` is algebraic, when viewed as an element of the `R`-algebra `A`. -/
+lemma is_algebraic_algebra_map (a : R) : is_algebraic R (algebra_map R A a) :=
+⟨X - C a, X_sub_C_ne_zero a, by simp only [aeval_C, aeval_X, alg_hom.map_sub, sub_self]⟩
+
 end zero_ne_one
 
 section field