docs(overview, undergrad): add Liouville's Theorem on existence of tr…

…anscendental numbers (#8068) Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>
leanprover-community · Jun 25, 2021 · 10cd252 · 10cd252
1 parent 2608244
commit 10cd252
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 2 deletions.
diff --git a/docs/overview.yaml b/docs/overview.yaml
@@ -128,6 +128,8 @@ General algebra:
     "Hensel's lemma (for $\\mathbb{Z}_p$)": 'hensels_lemma'
     ring of Witt vectors: 'witt_vector'
     perfection of a ring: 'ring.perfection'
+  Transcendental numbers:
+    Liouville's theorem on existence of transcendental numbers: liouville.is_transcendental
 
 Linear algebra:
   Fundamentals:

diff --git a/docs/undergrad.yaml b/docs/undergrad.yaml
@@ -180,7 +180,7 @@ Ring Theory:
     $\C$ is algebraically closed: 'complex.exists_root'
     field of fractions of an integral domain: 'fraction_map'
     algebraic elements: 'is_algebraic'
-    transcendental elements:
+    transcendental elements: 'transcendental'
     algebraic extensions: 'algebra.is_algebraic'
     algebraically closed fields: 'is_alg_closed'
     rupture fields: 'adjoin_root'

diff --git a/src/analysis/liouville/basic.lean → src/number_theory/liouville/basic.lean b/src/analysis/liouville/basic.lean → src/number_theory/liouville/basic.lean
diff --git a/...nalysis/liouville/liouville_constant.lean → ..._theory/liouville/liouville_constant.lean b/...nalysis/liouville/liouville_constant.lean → ..._theory/liouville/liouville_constant.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Jujian Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa, Jujian Zhang
 -/
-import analysis.liouville.basic
+import number_theory.liouville.basic
 /-!
 
 # Liouville constants