diff --git a/src/Frobenius.lean b/src/Frobenius.lean
index 2342c6af..cb78473a 100644
--- a/src/Frobenius.lean
+++ b/src/Frobenius.lean
@@ -1,14 +1,62 @@
 import algebra.char_p
 import for_mathlib.primes
+import for_mathlib.char_p
+import for_mathlib.ideal_operations
 
 /-!
 The main purpose of this file is to introduce notation that
 is not available in mathlib, and that we don't want to set up in the main file.
 -/
 
-/--The Frobenius endomorphism of a semiring-/
-noncomputable def Frobenius (α : Type*) [semiring α] : α → α := λ x, x^(ring_char α)
+-- /--The Frobenius endomorphism of a semiring-/
+-- noncomputable def Frobenius (α : Type*) [semiring α] : α → α := λ x, x^(ring_char α)
 
-notation `Frob` R `∕` x := Frobenius (ideal.quotient (ideal.span ({x} : set R)))
+notation `Frob` R `∕` p := frobenius (ideal.quotient (ideal.span ({p} : set R))) p
 
 notation x `∣` y `in` R := (x : R) ∣ (y : R)
+
+section
+open function
+
+variables (R : Type*) (A : Type*) [comm_ring R] [comm_ring A] [algebra R A] (p : nat.primes)
+
+lemma ring_char.eq_iff (n : ℕ) :
+  ring_char R = n ↔ char_p R n :=
+begin
+  split,
+  { rintro rfl, exact ring_char.char R },
+  { intro h, exact (ring_char.eq R h).symm }
+end
+
+def char_p.zmodp_algebra [hp : char_p R p] : algebra (zmodp p p.2) R :=
+algebra.of_ring_hom zmod.cast (@zmod.cast_is_ring_hom R _ ⟨p,_⟩ hp)
+
+instance zmod.char_p (n : ℕ+) : char_p (zmod n) n :=
+⟨λ k, zmod.eq_zero_iff_dvd_nat⟩
+
+instance zmodp.char_p (p : ℕ) (hp : p.prime) : char_p (zmodp p hp) p :=
+zmod.char_p ⟨p, _⟩
+
+lemma char_p_algebra [hp : char_p R p] (h : (0:A) ≠ 1) : char_p A p :=
+begin
+  letI := char_p.zmodp_algebra R,
+  letI : nonzero_comm_ring (algebra.comap (zmodp p p.2) R A) :=
+  { zero_ne_one := h, .. ‹comm_ring A› },
+  change char_p (algebra.comap (zmodp p p.2) R A) p,
+  convert char_p_algebra_over_field (zmodp p p.2),
+  { exact algebra.comap.algebra _ _ _ },
+  { apply_instance }
+end
+
+lemma frobenius_surjective_of_char_p [hp : char_p R p] (h : surjective (frobenius R p)) :
+  surjective (Frob R∕p) :=
+begin
+  rintro ⟨x⟩,
+  rcases h x with ⟨y, rfl⟩,
+  refine ⟨ideal.quotient.mk _ y, _⟩,
+  delta frobenius,
+  rw ← ideal.quotient.mk_pow,
+  refl,
+end
+
+end
diff --git a/src/Spa/localization_Huber.lean b/src/Spa/localization_Huber.lean
index 98be980d..70e917ac 100644
--- a/src/Spa/localization_Huber.lean
+++ b/src/Spa/localization_Huber.lean
@@ -108,7 +108,7 @@ begin
 end
 
 /--The natural map from the localization A⟮T/s⟯ of a Huber pair A
-at a rational open subset D(T/s)
+at a rational open subset R(T/s)
 to the valuation field of a valuation that does not have s in its support.-/
 noncomputable def to_valuation_field (hs : v s ≠ 0) : A⟮T/s⟯ → (valuation_field v) :=
 Huber_ring.away.lift T s (valuation_field_mk v) (unit_s hs) rfl
@@ -149,13 +149,13 @@ lemma to_valuation_field_cts_aux {r : spa.rational_open_data A} {v : spa A}
 (hv : v ∈ r.open_set) : (Spv.out v.1) (r.s) ≠ 0 := hv.2
 
 /-- The natural map from A(T/s) to the valuation field of a valuation v contained in
-the rational open subset D(T/s). -/
+the rational open subset R(T/s). -/
 def to_valuation_field {r : spa.rational_open_data A} {v : spa A} (hv : v ∈ r.open_set) :
   spa.rational_open_data.localization r → valuation_field (Spv.out (v.val)) :=
 (to_valuation_field $ to_valuation_field_cts_aux hv)
 
 /-- The natural map from A(T/s) to the valuation field of a valuation v contained in
-the rational open subset D(T/s) is a ring homomorphism. -/
+the rational open subset R(T/s) is a ring homomorphism. -/
 instance {r : spa.rational_open_data A} {v : spa A} (hv : v ∈ r.open_set) :
   is_ring_hom (to_valuation_field hv) := by {delta to_valuation_field, apply_instance}
 
diff --git a/src/Spa/stalk_valuation.lean b/src/Spa/stalk_valuation.lean
index d1375bee..ed5f0252 100644
--- a/src/Spa/stalk_valuation.lean
+++ b/src/Spa/stalk_valuation.lean
@@ -32,7 +32,7 @@ and define the map on the sections s in F(U) for open neigbourhoods U of x.
 But we have to check a compatibility condition, and this takes some effort.
 
 Let us translate this to the context of the structure presheaf of the adic spectrum.
-The sections above a rational open subset D(T/s) are:
+The sections above a rational open subset R(T/s) are:
 
   rat_open_data_completion r := A<T/s>
 
@@ -56,7 +56,7 @@ local attribute [instance] valued.uniform_space
 namespace rational_open_data
 
 /-- The natural map from A<T/s> to the completion of the valuation field of a valuation v
-contained in D(T/s). -/
+contained in R(T/s). -/
 noncomputable def to_complete_valuation_field (r : rational_open_data A) {v : spa A}
   (hv : v ∈ r.open_set) :
   rat_open_data_completion r → completion (valuation_field (Spv.out v.1)) :=
@@ -65,7 +65,7 @@ completion.map (Huber_pair.rational_open_data.to_valuation_field hv)
 variables {r r1 r2 : rational_open_data A} {v : spa A} (hv : v ∈ r.open_set)
 
 /-- The natural map from A<T/s> to the completion of the valuation field of a valuation v
-contained in D(T/s) is a ring homomorphism. -/
+contained in R(T/s) is a ring homomorphism. -/
 instance to_complete_valuation_field_is_ring_hom :
   is_ring_hom (r.to_complete_valuation_field hv) :=
 completion.is_ring_hom_map (Huber_pair.rational_open_data.to_valuation_field_cts hv)
diff --git a/src/examples/char_p.lean b/src/examples/char_p.lean
new file mode 100644
index 00000000..5038291d
--- /dev/null
+++ b/src/examples/char_p.lean
@@ -0,0 +1,342 @@
+import ring_theory.power_series
+import algebra.char_p algebra.group_power
+
+import for_mathlib.nnreal
+import for_mathlib.char_p
+
+import valuation.perfection
+import perfectoid_space
+import perfectoid_field
+
+noncomputable theory
+open_locale classical
+open function
+
+local postfix `ᵒ` : 66 := power_bounded_subring
+
+local attribute [instance] nnreal.pow_enat
+
+namespace power_series
+variables (K : Type*) [discrete_field K]
+
+def valuation (b : {r : nnreal // 0 < r ∧ r < 1}) : valuation (power_series K) nnreal :=
+{ to_fun := λ φ, b ^ φ.order,
+  map_zero' := by rw [order_zero, nnreal.pow_enat_top],
+  map_one' := by rw [order_one, nnreal.pow_enat_zero],
+  map_mul' := λ x y, by rw [order_mul, nnreal.pow_enat_add],
+  map_add' := λ x y,
+  begin
+    have : _ ≤ _ := order_add_ge x y,
+    rw min_le_iff at this,
+    rw le_max_iff,
+    have b_ne_zero : (b : nnreal) ≠ 0 := ne_of_gt b.2.left,
+    cases this with h h; [left, right],
+    all_goals
+    { apply nnreal.pow_enat_le _ b_ne_zero _ _ _ h,
+      exact le_of_lt b.2.right, },
+  end }
+
+end power_series
+
+/- The following definition is mathematically correct,
+but probably not the version that we want to put into mathlib.
+We make it for the sole purpose of constructing a perfectoid field.-/
+def laurent_series (K : Type*) [discrete_field K] := localization.fraction_ring (power_series K)
+
+namespace laurent_series
+variables (p : nat.primes) (K : Type*) [discrete_field K]
+
+instance : discrete_field (laurent_series K) := by delta laurent_series; apply_instance
+
+def algebra : algebra K (laurent_series K) :=
+algebra.of_ring_hom (localization.of ∘ power_series.C K) $
+@is_ring_hom.comp _ _ _ _ (power_series.C K) (ring_hom.is_ring_hom _)
+  _ _ localization.of localization.of.is_ring_hom
+
+variables [char_p K p]
+
+def valuation (b : {r : nnreal // 0 < r ∧ r < 1}) : valuation (laurent_series K) nnreal :=
+valuation.localization (power_series.valuation K b) $ λ φ h,
+begin
+  rw localization.fraction_ring.mem_non_zero_divisors_iff_ne_zero at h,
+  contrapose! h,
+  change (_ : nnreal) ^ φ.order = 0 at h,
+  have b_ne_zero : (b : nnreal) ≠ 0 := ne_of_gt b.2.left,
+  rw ← power_series.order_eq_top,
+  apply (nnreal.pow_enat_inj _ b_ne_zero b.2.right),
+  rwa nnreal.pow_enat_top,
+end
+
+lemma non_trivial (b : {r : nnreal // 0 < r ∧ r < 1}) : ¬ (valuation K b).is_trivial :=
+begin
+  have b_ne_zero : (b : nnreal) ≠ 0 := ne_of_gt b.2.left,
+  assume H, cases H (localization.of (power_series.X)) with h h;
+  erw valuation.localization_apply at h; change _ ^ _ = _ at h,
+  { apply b_ne_zero,
+    simpa only [nnreal.pow_enat_one, power_series.order_X] using h },
+  { simp only [nnreal.pow_enat_one, power_series.order_X] at h,
+    exact ne_of_lt b.2.right h, },
+end
+
+local attribute [instance] algebra
+
+instance [char_p K p] : char_p (laurent_series K) p :=
+char_p_algebra_over_field K
+
+end laurent_series
+
+def laurent_series_perfection (K : Type*) [discrete_field K] :=
+perfect_closure (laurent_series K) (ring_char K)
+
+namespace laurent_series_perfection
+variables (p : nat.primes) (K : Type*) [discrete_field K] [hp : char_p K p]
+include hp
+
+instance : discrete_field (laurent_series_perfection K) :=
+@perfect_closure.discrete_field (laurent_series K) _ _ (ring_char.prime p K) $
+by { rw ← ring_char.eq K hp, apply_instance }
+
+def valuation (b : {r : nnreal // 0 < r ∧ r < 1}) :
+  valuation (laurent_series_perfection K) nnreal :=
+@valuation.perfection (laurent_series K) _ (laurent_series.valuation K b)
+(ring_char K) (ring_char.prime p _) $
+by { rw ← ring_char.eq K hp, apply_instance }
+
+lemma non_discrete (b : {r : nnreal // 0 < r ∧ r < 1}) (ε : nnreal) (h : 0 < ε) :
+  ∃ x : laurent_series_perfection K, 1 < valuation p K b x ∧ valuation p K b x < 1 + ε :=
+@valuation.perfection.non_discrete _ _ _ (ring_char.prime p _)
+(by { rw ← ring_char.eq K hp, apply_instance }) _ (laurent_series.non_trivial K b) ε h
+
+lemma non_trivial (b : {r : nnreal // 0 < r ∧ r < 1}) : ¬ (valuation p K b).is_trivial :=
+begin
+  rcases non_discrete p K b 2 (by norm_num) with ⟨x, h₁, h₂⟩,
+  contrapose! h₁, cases h₁ x with h h; rw h,
+  exact zero_le _,
+end
+
+lemma frobenius_surjective : surjective (frobenius (laurent_series_perfection K) p) :=
+begin
+  rw ring_char.eq K hp,
+  let F := (perfect_closure.frobenius_equiv (laurent_series K) _),
+  { exact F.surjective },
+  { exact ring_char.prime p K },
+  { rw ← ring_char.eq K hp, apply_instance }
+end
+
+def algebra : algebra (laurent_series K) (laurent_series_perfection K) :=
+algebra.of_ring_hom (perfect_closure.of _ _) $
+@perfect_closure.is_ring_hom _ _ _ (ring_char.prime _ _) $
+by { rw ← ring_char.eq K hp, apply_instance }
+
+end laurent_series_perfection
+
+namespace laurent_series_perfection
+-- Now we take K in universe Type. For example `valued` requires this.
+variables (p : nat.primes) (K : Type) [discrete_field K] [char_p K p]
+include p
+
+protected def valued (b : {r : nnreal // 0 < r ∧ r < 1}) : valued (laurent_series_perfection K) :=
+{ Γ₀ := nnreal, v := valuation p K b }
+
+def valued_p : valued (laurent_series_perfection K) :=
+laurent_series_perfection.valued p K ⟨p⁻¹,
+begin
+  have p_inv_ne_zero : (p⁻¹ : nnreal) ≠ 0,
+  { assume H, apply p.ne_zero,
+    rw [← inv_inj'', inv_zero', inv_inv'', eq_comm, (show (p:nnreal) = (p:ℕ), by rw coe_coe)] at H,
+    exact_mod_cast H.symm, },
+  split,
+  { exact lt_of_le_of_ne (zero_le _) p_inv_ne_zero.symm, },
+  { rw [← linear_ordered_structure.inv_lt_inv, inv_one', inv_inv'',
+        (show (p:nnreal) = (p:ℕ), by rw coe_coe)],
+    { exact_mod_cast p.one_lt },
+    { exact one_ne_zero },
+    { exact p_inv_ne_zero } }
+end⟩
+
+end laurent_series_perfection
+
+def vlsp (K : Type) [discrete_field K] (b : {r : nnreal // 0 < r ∧ r < 1}) :=
+laurent_series_perfection K
+
+namespace vlsp
+variables (p : nat.primes) (K : Type) [discrete_field K] [char_p K p]
+variables (b : {r : nnreal // 0 < r ∧ r < 1})
+include p
+
+instance : discrete_field (vlsp K b) :=
+laurent_series_perfection.discrete_field p K
+
+local attribute [instance] valued.subgroups_basis subgroups_basis.topology
+  ring_filter_basis.topological_ring valued.uniform_space
+
+instance : valued (vlsp K b) := laurent_series_perfection.valued p K b
+
+
+
+end vlsp
+
+section
+open uniform_space
+variables (p : nat.primes) (K : Type) [discrete_field K] [char_p K p]
+include p
+
+local attribute [instance] valued.subgroups_basis subgroups_basis.topology
+  ring_filter_basis.topological_ring valued.uniform_space laurent_series_perfection.valued_p
+
+/-- The completion of the perfection of the Laurent series over a field. -/
+def clsp := completion (laurent_series_perfection K)
+
+end
+
+section char_p_completion
+open uniform_space
+variables {R : Type*} [comm_ring R] [uniform_space R] [uniform_add_group R] [separated R]
+  [topological_ring R] (p : nat.primes) [char_p R p]
+
+instance completion.char_p : char_p (completion R) p :=
+(subring_char_p p (completion.uniform_embedding_coe R).inj).mpr ‹_›
+
+end char_p_completion
+
+section
+open uniform_space
+--variables (K : Type*) [discrete_field K] [topological_space K] [topological_division_ring K]
+variables {G : Type*} [add_comm_group G] [uniform_space G] [uniform_add_group G]
+variables {H : Type*} [add_comm_group H] [uniform_space H] [uniform_add_group H]
+variables {φ : G → H} {ψ : H → G} (h : φ ∘ ψ = id) [is_add_group_hom φ] [is_add_group_hom ψ]
+  (hφ : continuous φ) (hψ : continuous ψ)
+include h hφ hψ
+local notation `hat` x:90 := completion.map x
+
+lemma johan : surjective hat φ :=
+have key : hat φ ∘ hat ψ = id,
+  by { rw [← completion.map_id, ← h],
+       exact completion.map_comp (uniform_continuous_of_continuous hφ)
+                              (uniform_continuous_of_continuous hψ) },
+λ y, ⟨(hat ψ) y, congr_fun key _⟩
+end
+
+namespace uniform_space.completion
+open uniform_space
+variables {α : Type*} [ring α] [uniform_space α] [topological_ring α] [uniform_add_group α]
+
+local infix `^` := monoid.pow
+
+@[move_cast]
+lemma coe_pow (a : α) (n : ℕ) : ((a^n : α) : completion α) = a^n :=
+begin
+  induction n with n ih,
+  exact completion.coe_one _,
+  change ↑(a*a^n) = ↑a*↑a^n,
+  rw [coe_mul, ih],
+end
+end uniform_space.completion
+
+section
+open uniform_space
+variables (p : nat.primes) (K : Type) [discrete_field K] [char_p K p] [uniform_space K]
+  [uniform_add_group K] [topological_division_ring K] [separated K]
+
+lemma completion.frobenius_eq : frobenius (completion K) p = completion.map (frobenius K p) :=
+begin
+  symmetry,
+  apply completion.map_unique,
+  { haveI hom : is_ring_hom (frobenius (completion K) p) := by {
+    apply frobenius.is_ring_hom _,
+    exact p.property,
+    exact completion.char_p _,
+  },
+    haveI : topological_monoid (completion K) := topological_ring.to_topological_monoid _,
+    exact uniform_continuous_of_continuous (continuous_pow p)
+    },
+  { intro x,
+    simp [frobenius],
+    erw completion.coe_pow,
+    refl }
+end
+end
+
+namespace clsp
+open uniform_space
+variables (p : nat.primes) (K : Type) [discrete_field K] [char_p K p]
+include p
+
+local attribute [instance] valued.subgroups_basis subgroups_basis.topology
+  ring_filter_basis.topological_ring valued.uniform_space valued.uniform_add_group
+  laurent_series_perfection.valued_p
+
+instance : discrete_field (clsp p K) := completion.discrete_field
+instance : uniform_space (clsp p K) := completion.uniform_space _
+instance : topological_division_ring (clsp p K) := completion.topological_division_ring
+instance : complete_space (clsp p K) := completion.complete_space _
+instance : separated (clsp p K) := completion.separated _
+
+def valuation : valuation (clsp p K) nnreal := valued.extension_valuation
+
+lemma frobenius_surjective : surjective (frobenius (clsp p K) p) :=
+begin
+  dsimp [clsp],
+  set lsp := (laurent_series_perfection K),
+  haveI char : char_p lsp ↑p := sorry,
+  rw completion.frobenius_eq,
+  obtain ⟨ψ, inv, cont⟩ : ∃ ψ : (laurent_series_perfection K) → (laurent_series_perfection K),
+    (frobenius lsp p) ∘ ψ = id ∧ continuous ψ,
+  {
+    sorry },
+
+  sorry
+end
+
+-- instance laurent_series_valued : valued (laurent_series K) :=
+-- { Γ₀ := nnreal, v := laurent_series.valuation p K }
+
+-- protected def algebra : algebra (laurent_series_perfection K) (clsp p K) :=
+-- algebra.of_ring_hom
+--   (coe : (laurent_series_perfection K) → completion (laurent_series_perfection K)) $
+-- @completion.is_ring_hom_coe (laurent_series_perfection K) _ _ _ $
+-- @valued.uniform_add_group (laurent_series_perfection K) _ $ laurent_series_perfection.valued p K
+
+-- def rod_algebra : algebra (power_series K) (clsp p K) :=
+-- @algebra.comap.algebra _ _ _ _ _ _ _ $
+-- @algebra.comap.algebra (laurent_series K) (laurent_series_perfection K) (clsp p K) _ _ _
+-- (laurent_series_perfection.algebra p K) (clsp.algebra p K)
+
+-- def rod : Huber_ring.ring_of_definition (laurent_series K) (clsp p K) :=
+-- {
+--   .. rod_algebra p K }
+
+-- def Huber_ring : Huber_ring (clsp p K) :=
+-- { pod :=
+--   begin
+--   end }
+
+-- instance : perfectoid_field p (clsp p K) :=
+-- { v := valuation p K,
+--   non_discrete := λ ε h,
+--   begin
+--     choose x hx using laurent_series_perfection.non_discrete p K ε h,
+--     delta clsp, use x,
+--     convert hx using 2; exact valued.extension_extends _
+--   end,
+--   Frobenius :=
+--   begin
+--     apply @surjective.of_comp _ _ _ _ (ideal.quotient.mk _) _,
+--     conv {congr, simp only [frobenius, comp], funext, rw [← ideal.quotient.mk_pow]},
+--     apply surjective_comp,
+--     { rintro ⟨x⟩, exact ⟨x, rfl⟩ },
+--     intro x,
+--     choose y hy using frobenius_surjective p K x.val,
+--     have hvy : valuation p K y ≤ 1,
+--     { have aux := congr_arg (valuation p K) hy,
+--       replace hy := x.property,
+--       rw [← aux, frobenius, valuation.map_pow] at hy, clear aux,
+--       apply linear_ordered_structure.le_one_of_pow_le_one _ _ hy,
+--       exact_mod_cast p.ne_zero, },
+--     refine ⟨⟨y, hvy⟩, _⟩,
+--     { rw [subtype.ext], convert hy,
+--       convert @is_semiring_hom.map_pow _ _ _ _ subtype.val _ ⟨y,_⟩ p,
+--        }
+--   end }
+
+end clsp
diff --git a/src/examples/valuations.lean b/src/examples/valuations.lean
new file mode 100644
index 00000000..04272b32
--- /dev/null
+++ b/src/examples/valuations.lean
@@ -0,0 +1,115 @@
+/-
+Stuff in this file should eventually go to the valuation folder,
+but keeping it here is faster at this point.
+-/
+
+import valuation.basic
+import valuation.topology
+
+local attribute [instance, priority 0] classical.decidable_linear_order
+
+section
+@[elab_as_eliminator] protected lemma pnat.induction_on {p : ℕ+ → Prop}
+  (i : ℕ+) (hz : p 1) (hp : ∀j : ℕ+, p j → p (j + 1)) : p i :=
+begin
+  cases i with i hi,
+  rcases nat.exists_eq_succ_of_ne_zero (ne_of_gt hi) with ⟨i, rfl⟩,
+  induction i with i IH, {assumption},
+  have h : 0 < i + 1, {exact nat.succ_pos i},
+  apply hp ⟨i+1, h⟩,
+  exact IH _,
+end
+
+variables (Γ₀ : Type*)  [linear_ordered_comm_group_with_zero Γ₀]
+open  linear_ordered_structure
+
+lemma linear_ordered_comm_group_with_zero.pow_strict_mono (n : ℕ+) : strict_mono (λ x : Γ₀, x^(n : ℕ)) :=
+begin
+  intros x y h,
+  induction n using pnat.induction_on with n ih, { simpa },
+  { dsimp only [] at *,
+    rw [pnat.add_coe, pnat.one_coe, pow_succ, pow_succ], -- here we miss some norm_cast attribute
+    apply linear_ordered_structure.mul_lt_mul' h ih, }
+end
+
+lemma linear_ordered_comm_group_with_zero.pow_mono (n : ℕ+) : monotone (λ x : Γ₀, x^(n : ℕ)) :=
+(linear_ordered_comm_group_with_zero.pow_strict_mono Γ₀ n).monotone
+
+variables {Γ₀}
+lemma linear_ordered_comm_group_with_zero.pow_le_pow {x y : Γ₀} {n : ℕ+} : x^(n : ℕ) ≤ y^(n : ℕ) ↔ x ≤ y :=
+strict_mono.le_iff_le (linear_ordered_comm_group_with_zero.pow_strict_mono Γ₀ n)
+
+end
+
+namespace valuation
+variables {R : Type*} [ring R]
+variables {Γ₀   : Type*} [linear_ordered_comm_group_with_zero Γ₀]
+variables {Γ'₀   : Type*} [linear_ordered_comm_group_with_zero Γ'₀]
+variables (v : valuation R Γ₀)
+
+instance : has_pow (valuation R Γ₀) ℕ+ :=
+⟨λ v n, { to_fun := λ r, (v r)^(n : ℕ),
+  map_one' := by rw [v.map_one, one_pow],
+  map_mul' := λ x y, by rw [v.map_mul, mul_pow],
+  map_zero' := show (v 0)^n.val = 0,
+    by rw [valuation.map_zero, ← nat.succ_pred_eq_of_pos n.2, pow_succ, zero_mul],
+  map_add' := begin
+    intros x y,
+    wlog vyx : v y ≤ v x using x y,
+    { have : (v y)^(n:ℕ) ≤ (v x)^(n:ℕ),
+        by apply linear_ordered_comm_group_with_zero.pow_mono ; assumption,
+      rw max_eq_left this,
+      apply linear_ordered_comm_group_with_zero.pow_mono,
+      convert v.map_add x y,
+      rw max_eq_left vyx },
+    { rwa [add_comm, max_comm] },
+  end }⟩
+
+@[simp] protected lemma pow_one : v^(1:ℕ+) = v :=
+ext $ λ r, pow_one (v r)
+
+protected lemma pow_mul (m n : ℕ+) : v^(m*n) = (v^m)^n :=
+ext $ λ r, pow_mul (v r) m n
+
+lemma is_equiv_pow_pow (v : valuation R Γ₀) (m n : ℕ+) : is_equiv (v^m) (v^n) :=
+begin
+  intros r s,
+  change (v r) ^ (m:ℕ) ≤ (v s) ^ (m:ℕ) ↔ _,
+  rw [← linear_ordered_comm_group_with_zero.pow_le_pow, ← pow_mul, ← pow_mul,
+      mul_comm, pow_mul, pow_mul, linear_ordered_comm_group_with_zero.pow_le_pow],
+  { exact iff.rfl }
+end
+
+lemma is_equiv_pow_self (v : valuation R Γ₀) (n : ℕ+) : is_equiv v (v^n) :=
+by simpa using v.is_equiv_pow_pow 1 n
+
+namespace is_equiv
+
+open_locale uniformity
+
+lemma uniformity_eq_aux (h₁ : valued R) (h₂ : valued R) (h : h₁.v.is_equiv h₂.v) :
+  @valued.uniform_space R _ h₁ ≤ id (@valued.uniform_space R _ h₂) :=
+begin
+  rw ← uniform_space_comap_id,
+  rw ← uniform_continuous_iff,
+  apply @uniform_continuous_of_continuous R R
+    (@valued.uniform_space R _ h₁) _ (@valued.uniform_add_group R _ h₁)
+    (@valued.uniform_space R _ h₂) _ (@valued.uniform_add_group R _ h₂),
+  apply @topological_add_group.continuous_of_continuous_at_zero _ _ _ _ _ _ _ _ _ _ _,
+  any_goals { apply_instance },
+  { exact @uniform_add_group.to_topological_add_group R (@valued.uniform_space R _ h₁) _ (@valued.uniform_add_group R _ h₁), },
+  { exact @uniform_add_group.to_topological_add_group R (@valued.uniform_space R _ h₂) _ (@valued.uniform_add_group R _ h₂), },
+  { intros U,
+    rw [id.def, filter.map_id, valued.mem_nhds_zero, (@valued.mem_nhds_zero R _ h₁ U)],
+    rintros ⟨γ, hU⟩,
+    sorry -- is this provable with the current definitions??
+    },
+end
+
+lemma uniformity_eq (h₁ : valued R) (h₂ : valued R) (h : h₁.v.is_equiv h₂.v) :
+  @valued.uniform_space R _ h₁ = @valued.uniform_space R _ h₂ :=
+le_antisymm (h.uniformity_eq_aux h₁ h₂) (h.symm.uniformity_eq_aux h₂ h₁)
+
+end is_equiv
+
+end valuation
diff --git a/src/for_mathlib/char_p.lean b/src/for_mathlib/char_p.lean
new file mode 100644
index 00000000..33a5628d
--- /dev/null
+++ b/src/for_mathlib/char_p.lean
@@ -0,0 +1,148 @@
+import algebra.char_p
+import ring_theory.algebra
+import ring_theory.ideal_operations
+import ring_theory.principal_ideal_domain
+
+open function
+
+lemma map_nat_cast {α : Type*} {β : Type*} [semiring α] [semiring β]
+  (f : α → β) [is_semiring_hom f] (n : ℕ) :
+  f n = n :=
+begin
+  induction n with n ih, { exact is_semiring_hom.map_zero f },
+  rw [nat.cast_succ, nat.cast_succ, is_semiring_hom.map_add f, ih, is_semiring_hom.map_one f],
+end
+
+
+section
+variables (p : nat.primes) (R : Type*) [semiring R] [char_p R p]
+include p
+
+lemma ring_char.prime : nat.prime (ring_char R) :=
+by { rw ← ring_char.eq R ‹_›, exact p.2 }
+
+end
+
+instance ring_char.char (R : Type*) [semiring R] : char_p R (ring_char R) :=
+{ cast_eq_zero_iff := ring_char.spec R }
+
+section
+variables {K : Type*} {R : Type*} {p : ℕ} [discrete_field K] [nonzero_comm_ring R] [algebra K R]
+
+-- is_field_hom.injective is not general enough
+lemma hom_injective (f : K → R) [is_ring_hom f] : injective f :=
+begin
+  apply (is_ring_hom.inj_iff_ker_eq_bot f).mpr,
+  apply classical.or_iff_not_imp_right.mp (ideal.eq_bot_or_top _),
+  rw ideal.eq_top_iff_one,
+  exact is_ring_hom.not_one_mem_ker f,
+end
+
+variable (K)
+
+lemma char_p_algebra_over_field [char_p K p] : char_p R p :=
+{ cast_eq_zero_iff := λ n,
+  begin
+    have : injective (algebra_map R : K → R) := hom_injective _,
+    rw [← char_p.cast_eq_zero_iff K, ← this.eq_iff, algebra.map_zero,
+      map_nat_cast (algebra_map R : K → R)],
+  end }
+end
+
+section char_p_subring
+open int
+variables {R : Type*} [comm_ring R]
+
+lemma nat.eq_of_dvd {p q : ℕ} (h : p ∣ q) (h' : q ∣ p) : p = q :=
+begin
+  cases h with n hn,
+  cases h' with m hm,
+  cases nat.eq_zero_or_pos p,
+    simp [h, hn],
+  rw [hn, mul_assoc, eq_comm, nat.mul_right_eq_self_iff h, nat.mul_eq_one_iff] at hm,
+  simp [hn, hm.1],
+end
+
+lemma int.nat_abs_dvd_iff {p : ℤ} {n : ℕ} : nat_abs p ∣ n ↔ p ∣ n :=
+begin
+  split; intro h,
+    refine dvd_trans _ (coe_nat_dvd.mpr h), rw dvd_nat_abs,
+  rw ←coe_nat_dvd,
+  refine dvd_trans _ h,
+  rw nat_abs_dvd,
+end
+
+lemma cast_nat_abs_zero (k : ℤ) (h : (k : R) = 0) :  (nat_abs k : R) = 0 :=
+begin
+  cases nat_abs_eq k with hpos hneg,
+    show (((nat_abs k) : ℤ) : R) = 0,
+    rwa ←hpos,
+  show (((nat_abs k) : ℤ) : R) = 0,
+  rw eq_neg_of_eq_neg hneg,
+  simp [h],
+end
+
+variables {S : Type*} [comm_ring S] {φ : R → S} [is_ring_hom φ]
+
+lemma int.cast_ump : (int.cast : ℤ → S) = φ ∘ (int.cast : ℤ → R) :=
+begin
+  ext k,
+  induction k using int.induction_on with k ih k ih,
+  { simp,
+    change ((0 : ℤ) : S) = φ ((0 : ℤ) : R),
+    rw [int.cast_zero, int.cast_zero, is_ring_hom.map_zero φ] },
+  { rw [is_ring_hom.map_add (int.cast : ℤ → S), ih,
+        is_ring_hom.map_add (φ ∘ (int.cast : ℤ → R)),
+        is_ring_hom.map_one (φ ∘ (int.cast : ℤ → R))],
+    simp,
+    exact int.cast_one },
+  { rw [is_ring_hom.map_sub (int.cast : ℤ → S), ih,
+        is_ring_hom.map_sub (φ ∘ (int.cast : ℤ → R)),
+        is_ring_hom.map_one (φ ∘ (int.cast : ℤ → R))],
+    simp,
+    exact int.cast_one }
+end
+
+variables {T : Type*} [comm_ring T] {ψ : S → T} [is_ring_hom ψ]
+open is_ring_hom
+
+lemma is_ring_hom.ker_eq_of_inj (h : injective ψ) : ker (ψ ∘ φ) = ker φ :=
+begin
+  ext x,
+  rw [mem_ker, mem_ker, comp_app, ←map_zero ψ],
+  exact ⟨λ H, h H, congr_arg ψ⟩
+end
+
+open ideal.is_principal
+
+lemma char_is_char : ring_char R = nat_abs (generator (is_ring_hom.ker (int.cast : ℤ → R))) :=
+begin
+  apply nat.eq_of_dvd,
+  { rw ← ring_char.spec R,
+    apply cast_nat_abs_zero,
+    have := generator_mem (is_ring_hom.ker (int.cast : ℤ → R)),
+    rwa is_ring_hom.mem_ker at this
+  },
+  { rw [int.nat_abs_dvd_iff, ← mem_iff_generator_dvd, is_ring_hom.mem_ker],
+    apply char_p.cast_eq_zero }
+end
+
+lemma subring_ring_char (h : injective φ) : ring_char R = ring_char S :=
+begin
+  rw [char_is_char, char_is_char],
+  suffices : is_ring_hom.ker (int.cast : ℤ → R) = is_ring_hom.ker (int.cast : ℤ → S), by rw this,
+  have : (int.cast : ℤ → S) = φ ∘ (int.cast : ℤ → R), from int.cast_ump,
+  simp only [this],
+  exact (is_ring_hom.ker_eq_of_inj h).symm
+end
+
+lemma char_p_ring_char (p : nat.primes) : char_p R p ↔ ring_char R = p :=
+⟨λ h, (ring_char.eq R h).symm, λ h, h ▸ (classical.some_spec (char_p.exists_unique R)).1⟩
+
+lemma subring_char_p (p : nat.primes) (h : injective φ) : char_p S p ↔ char_p R p :=
+begin
+  repeat { rw char_p_ring_char },
+  rwa subring_ring_char h
+end
+
+end char_p_subring
diff --git a/src/for_mathlib/group_with_zero.lean b/src/for_mathlib/group_with_zero.lean
index b3c22b01..87f96f81 100644
--- a/src/for_mathlib/group_with_zero.lean
+++ b/src/for_mathlib/group_with_zero.lean
@@ -214,6 +214,15 @@ end
 lemma pow_ne_zero {a : α} {n : ℕ} (h : a ≠ 0) : a^n ≠ 0 :=
 assume H, h $ eq_zero_of_pow_eq_zero H
 
+lemma zero_pow (n : ℕ) (hn : n ≠ 0) : (0:α)^n = 0 :=
+begin
+  rcases nat.exists_eq_succ_of_ne_zero hn with ⟨n,rfl⟩,
+  rw [pow_succ, zero_mul], refl
+end
+
+lemma zero_pow_pnat (n : ℕ+) : (0:α)^(n:ℕ) = 0 :=
+zero_pow n (ne_of_gt n.2)
+
 theorem pow_sub (a : α) {m n : ℕ} (ha : a ≠ 0) (h : n ≤ m) : a^(m - n) = a^m * (a^n)⁻¹ :=
 have h1 : m - n + n = m, from nat.sub_add_cancel h,
 have h2 : a^(m - n) * a^n = a^m, by rw [←pow_add, h1],
diff --git a/src/for_mathlib/nnreal.lean b/src/for_mathlib/nnreal.lean
index 666a3dcd..e54200db 100644
--- a/src/for_mathlib/nnreal.lean
+++ b/src/for_mathlib/nnreal.lean
@@ -47,4 +47,119 @@ noncomputable instance : linear_ordered_comm_group_with_zero nnreal :=
   .. (infer_instance : linear_order nnreal),
   .. (infer_instance : comm_semiring nnreal) }
 
+section pow_enat
+noncomputable theory
+open_locale classical
+open function
+
+/--If r is a nonnegative real number and n an enat,
+than b^n is defined as expected if n is natural, and b^infty = 0.
+Hence, this should only be applied to b < 1.-/
+def pow_enat : has_pow nnreal enat :=
+⟨λ r n, if h : n.dom then (r^n.get h) else 0⟩
+
+local attribute [instance] pow_enat
+
+lemma pow_enat_def {b : nnreal} {n : enat} :
+  b^n = if h : n.dom then (b^n.get h) else 0 := rfl
+
+@[simp] lemma pow_enat_top (b : nnreal) :
+  b ^ (⊤ : enat) = 0 :=
+begin
+  rw [pow_enat_def, dif_neg], exact not_false
+end
+
+@[simp] lemma pow_enat_zero (b : nnreal) :
+  b ^ (0 : enat) = 1 :=
+begin
+  rw [pow_enat_def, dif_pos, enat.get_zero, pow_zero],
+  exact trivial,
+end
+
+@[simp] lemma pow_enat_one (b : nnreal) :
+  b ^ (1 : enat) = b :=
+begin
+  rw [pow_enat_def, dif_pos, enat.get_one, pow_one],
+  exact trivial,
+end
+
+@[simp] lemma pow_enat_add (b : nnreal) (m n : enat) :
+  b ^ (m + n) = b ^ m * b ^ n :=
+begin
+  iterate 3 {rw pow_enat_def},
+  by_cases hm : m.dom,
+  { by_cases hn : n.dom,
+    { have hmn : (m + n).dom := ⟨hm, hn⟩,
+      rw [dif_pos hm, dif_pos hn, dif_pos,
+          subtype.coe_ext, nnreal.coe_mul, ← nnreal.coe_mul, ← pow_add, enat.get_add, add_comm],
+      exact hmn, },
+    { rw [dif_pos hm, dif_neg hn, dif_neg, mul_zero],
+      contrapose! hn with H, exact H.2 } },
+  { rw [dif_neg hm, dif_neg, zero_mul],
+    contrapose! hm with H, exact H.1 },
+end
+
+@[simp] lemma pow_enat_le (b : nnreal) (h₁ : b ≠ 0) (h₂ : b ≤ 1) (m n : enat) (h : m ≤ n) :
+  b ^ n ≤ b ^ m :=
+begin
+  iterate 2 {rw pow_enat_def},
+  by_cases hn : n.dom,
+  { rw ← enat.coe_get hn at h,
+    have hm : m.dom := enat.dom_of_le_some h,
+    rw [← enat.coe_get hm, enat.coe_le_coe] at h,
+    rw [dif_pos hm, dif_pos hn],
+    rw [← linear_ordered_structure.inv_le_inv _ h₁, inv_one'] at h₂,
+    have := pow_le_pow h₂ h,
+    -- We need lots of norm_cast lemmas
+    rwa [nnreal.coe_le, nnreal.coe_pow, nnreal.coe_pow, nnreal.coe_inv, ← pow_inv, ← pow_inv,
+      ← nnreal.coe_pow, ← nnreal.coe_pow, ← nnreal.coe_inv, ← nnreal.coe_inv, ← nnreal.coe_le,
+      linear_ordered_structure.inv_le_inv] at this,
+    any_goals { exact one_ne_zero },
+    all_goals { contrapose! h₁ },
+    any_goals { exact subtype.val_injective h₁ },
+    any_goals { apply group_with_zero.pow_eq_zero, assumption } },
+  { rw dif_neg hn, exact zero_le _ }
+end
+
+@[simp] lemma pow_enat_lt (b : nnreal) (h₁ : b ≠ 0) (h₂ : b < 1) (m n : enat) (h : m < n) :
+  b ^ n < b ^ m :=
+begin
+  iterate 2 {rw pow_enat_def},
+  by_cases hn : n.dom,
+  { rw ← enat.coe_get hn at h,
+    have hm : m.dom := enat.dom_of_le_some (le_of_lt h),
+    rw [← enat.coe_get hm, enat.coe_lt_coe] at h,
+    rw [dif_pos hm, dif_pos hn],
+    rw [← linear_ordered_structure.inv_lt_inv _ h₁, inv_one'] at h₂,
+    have := pow_lt_pow h₂ h,
+    -- We need lots of norm_cast lemmas
+    rwa [nnreal.coe_lt, nnreal.coe_pow, nnreal.coe_pow, nnreal.coe_inv, ← pow_inv, ← pow_inv,
+      ← nnreal.coe_pow, ← nnreal.coe_pow, ← nnreal.coe_inv, ← nnreal.coe_inv, ← nnreal.coe_lt,
+      linear_ordered_structure.inv_lt_inv] at this,
+    any_goals { exact one_ne_zero },
+    all_goals { contrapose! h₁ },
+    any_goals { exact subtype.val_injective h₁ },
+    all_goals { apply group_with_zero.pow_eq_zero, assumption } },
+  { rw dif_neg hn,
+    have : n = ⊤ := roption.eq_none_iff'.mpr hn, subst this,
+    replace h := ne_of_lt h,
+    rw enat.ne_top_iff at h, rcases h with ⟨m, rfl⟩,
+    rw dif_pos, swap, {trivial},
+    apply pow_pos,
+    exact lt_of_le_of_ne b.2 h₁.symm }
+end
+
+@[simp] lemma pow_enat_inj (b : nnreal) (h₁ : b ≠ 0) (h₂ : b < 1) :
+  injective ((^) b : enat → nnreal) :=
+begin
+  intros m n h,
+  wlog H : m ≤ n,
+  rcases lt_or_eq_of_le H with H|rfl,
+  { have := pow_enat_lt b h₁ h₂ m n H,
+    exfalso, exact ne_of_lt this h.symm, },
+  { refl },
+end
+
+end pow_enat
+
 end nnreal
diff --git a/src/for_mathlib/primes.lean b/src/for_mathlib/primes.lean
index daea8479..93b30679 100644
--- a/src/for_mathlib/primes.lean
+++ b/src/for_mathlib/primes.lean
@@ -1,7 +1,20 @@
 import data.nat.prime
 import ring_theory.ideals
 
-open nat
+import for_mathlib.char_p
+
+namespace nat
+namespace primes
+variable (p : primes)
 
 instance : has_coe primes ℕ := ⟨subtype.val⟩
-instance monoid.prime_pow {α : Type*} [monoid α]: has_pow α primes := ⟨λ x p, x^p.val⟩
+
+lemma ne_zero : (p : ℕ) ≠ 0 := p.2.ne_zero
+lemma ne_one : (p : ℕ) ≠ 1 := p.2.ne_one
+lemma one_lt : 1 < (p : ℕ) := p.2.one_lt
+lemma not_dvd_one : ¬ (p : ℕ) ∣ 1 := p.2.not_dvd_one
+
+end primes
+end nat
+
+instance monoid.prime_pow {α : Type*} [monoid α]: has_pow α nat.primes := ⟨λ x p, x^p.val⟩
diff --git a/src/perfectoid_field.lean b/src/perfectoid_field.lean
new file mode 100644
index 00000000..095ba057
--- /dev/null
+++ b/src/perfectoid_field.lean
@@ -0,0 +1,77 @@
+import for_mathlib.nnreal
+
+import valuation.topology
+import Huber_pair
+import Frobenius
+
+set_option old_structure_cmd true -- do we do this or not?
+
+namespace valuation
+variables {R : Type*} [comm_ring R]
+variables {Γ₀ : Type*} [linear_ordered_comm_group_with_zero Γ₀]
+
+local attribute [instance] classical.decidable_linear_order
+
+def le_one_subring (v : valuation R Γ₀) := {r : R | v r ≤ 1}
+
+instance le_one_subring.is_subring (v : valuation R Γ₀) : is_subring v.le_one_subring :=
+-- @subtype.comm_ring R _ {r : R | v r ≤ 1}
+{ zero_mem := show v 0 ≤ 1, by simp,
+  one_mem := show v 1 ≤ 1, by simp,
+  add_mem := λ r s (hr : v r ≤ 1) (hs : v s ≤ 1), show v (r+s) ≤ 1,
+  by calc v (r + s) ≤ max (v r) (v s) : v.map_add r s
+                ... ≤ 1 : max_le hr hs,
+  neg_mem := λ r (hr : v r ≤ 1), show v (-r) ≤ 1, by rwa [v.map_neg],
+  mul_mem := λ r s (hr : v r ≤ 1) (hs : v s ≤ 1), show v (r*s) ≤ 1,
+  begin
+    rw v.map_mul,
+    refine le_trans (actual_ordered_comm_monoid.mul_le_mul_right' hr) _,
+    rwa one_mul
+  end }
+
+instance coe_nat_le_one_subring (v : valuation R Γ₀) :
+  has_coe ℕ v.le_one_subring := by apply_instance
+
+end valuation
+
+class nondiscrete_valued_field (K : Type*) extends discrete_field K :=
+(v : valuation K nnreal)
+(non_discrete : ∀ ε : nnreal, 0 < ε → ∃ x : K, 1 < v x ∧ v x < 1 + ε)
+
+noncomputable instance foo {K : Type}
+  [nondiscrete_valued_field K] : valued K :=
+{ Γ₀ := nnreal,
+  v := nondiscrete_valued_field.v K}
+
+-- Currently we know that clsp is a complete uniform topological field.
+-- And this all comes from the completion machine
+
+open function nat
+
+local attribute [instance] valued.uniform_space valued.uniform_add_group
+local notation `v` := valued.value
+
+noncomputable example (K : Type) [nondiscrete_valued_field K] : uniform_space K
+:= by apply_instance
+
+-- separated should follow from the fact that the kernel of v is 0
+-- but I don't know how to steer it and I don't know if we need it.
+
+instance nondiscrete_valued_field.separated (K : Type) [nondiscrete_valued_field K] :
+  separated K := sorry
+
+local attribute [instance, priority 1000] comm_ring.to_ring
+
+class is_perfectoid_field (K : Type) [nondiscrete_valued_field K] (p : primes) : Prop :=
+[complete : complete_space K]
+(Frobenius : surjective (Frob (valued.v K).le_one_subring ∕p))
+
+-- Let K be the completion of the perfection of (Z/pZ)((t)). [done]
+-- Show that K is a perfectoid field
+-- show a perfectoid field is a perfectoid ring
+-- Show that Spa(K) is a perfectoid space.
+
+-- is a valued R a Huber ring?
+
+theorem perfectoid_field.huber_ring (K : Type) (p : primes)
+  [nondiscrete_valued_field K] [is_perfectoid_field K p] : Huber_ring K := sorry
diff --git a/src/valuation/basic.lean b/src/valuation/basic.lean
index 6a2a367a..c31dbb59 100644
--- a/src/valuation/basic.lean
+++ b/src/valuation/basic.lean
@@ -247,6 +247,22 @@ begin
   rwa [v₁.map_zero, v₂.map_zero] at this,
 end
 
+lemma eq_zero (h : v₁.is_equiv v₂) {r : R} :
+  v₁ r = 0 ↔ v₂ r = 0 :=
+by { rw [← v₁.map_zero, ← v₂.map_zero], exact h.val_eq }
+
+lemma eq_one (h : v₁.is_equiv v₂) {r : R} :
+  v₁ r = 1 ↔ v₂ r = 1 :=
+by { rw [← v₁.map_one, ← v₂.map_one], exact h.val_eq }
+
+lemma lt_iff (h : v₁.is_equiv v₂) {r s : R} :
+  v₁ r < v₁ s ↔ v₂ r < v₂ s :=
+by { have := not_iff_not_of_iff (h s r), push_neg at this, exact this }
+
+lemma lt_one (h : v₁.is_equiv v₂) {r : R} :
+  v₁ r < 1 ↔ v₂ r < 1 :=
+by { rw [← v₁.map_one, ← v₂.map_one], exact h.lt_iff }
+
 end is_equiv -- end of namespace
 
 lemma is_equiv_of_map_strict_mono [ring R] {v : valuation R Γ₀}
@@ -307,7 +323,17 @@ begin
   cases x; [left, {right, cases x}]; refl
 end
 
-lemma is_trivial_iff_val_le_one {K : Type*} [division_ring K] {v : valuation K Γ₀} :
+lemma is_equiv.is_trivial {v₁ : valuation R Γ₀} {v₂ : valuation R Γ'₀} (h : v₁.is_equiv v₂) :
+  v₁.is_trivial ↔ v₂.is_trivial :=
+begin
+  apply forall_congr, intro r,
+  exact or_congr h.eq_zero h.eq_one,
+end
+
+section division_ring
+variables {K : Type*} [division_ring K]
+
+lemma is_trivial_iff_val_le_one {v : valuation K Γ₀} :
   v.is_trivial ↔ ∀ x:K, v x ≤ 1 :=
 begin
   split; intros h x,
@@ -324,6 +350,23 @@ begin
     { push_neg at hx, exact ⟨_, hx⟩ } }
 end
 
+lemma exists_lt_one_of_not_trivial (v : valuation K Γ₀) (hv : ¬ v.is_trivial) :
+  ∃ x : K, v x < 1 ∧ v x ≠ 0 :=
+begin
+  delta is_trivial at hv, push_neg at hv, rcases hv with ⟨x, h₁, h₂⟩,
+  by_cases hx : v x < 1, { use [x, hx, h₁] },
+  use x⁻¹,
+  have xne : x ≠ 0, { rwa ← v.ne_zero_iff },
+  rw [v.map_inv' xne, ← linear_ordered_structure.inv_lt_inv _ _, inv_inv'', inv_one',
+      ← v.map_inv' xne, v.ne_zero_iff],
+  { push_neg at hx, replace hx := lt_of_le_of_ne hx (ne.symm h₂),
+    exact ⟨hx, inv_ne_zero xne⟩ },
+  { exact one_ne_zero },
+  { rw [← v.map_inv' xne, v.ne_zero_iff], exact inv_ne_zero xne },
+end
+
+end division_ring
+
 end trivial -- end of section
 
 section supp
diff --git a/src/valuation/discrete.lean b/src/valuation/discrete.lean
new file mode 100644
index 00000000..e570c2da
--- /dev/null
+++ b/src/valuation/discrete.lean
@@ -0,0 +1,58 @@
+import valuation.basic
+
+/-!
+# Discrete valuations
+
+We define discrete valuations
+-/
+
+universe variables u u₀ u₁
+
+open_locale classical
+
+namespace valuation
+variables {R : Type u} [ring R]
+variables {Γ₀   : Type u₀} [linear_ordered_comm_group_with_zero Γ₀]
+variables {Γ'₀  : Type u₁} [linear_ordered_comm_group_with_zero Γ'₀]
+variables (v : valuation R Γ₀) {v' : valuation R Γ'₀}
+
+/-- A valuation on a ring R is nondiscrete if for every element of R with value x < 1,
+there is another element of R whose value lies between x and 1. -/
+def is_non_discrete : Prop :=
+∀ r : R, v r < 1 → ∃ s : R, v r < v s ∧ v s < 1
+
+/-- A valuation on a ring R is discrete if there is an element x of the value monoid
+such that the valuation of every element of R is either 0 or an integer power of x. -/
+def is_discrete : Prop :=
+∃ r : R, ∀ s : R, v s ≠ 0 → ∃ n : ℤ, v s = (v r)^n
+
+namespace is_equiv
+variable {v}
+
+lemma is_non_discrete (h : v.is_equiv v') :
+  v.is_non_discrete ↔ v'.is_non_discrete :=
+begin
+  apply forall_congr, intro r,
+  apply imp_congr_ctx h.lt_one, intro hr,
+  apply exists_congr, intro s,
+  rw [h.lt_iff, h.lt_one]
+end
+
+-- This is not so trivial. But we don't need it atm.
+-- lemma is_discrete (h : v.is_equiv v') :
+--   v.is_discrete ↔ v'.is_discrete :=
+-- begin
+--   apply exists_congr, intro r,
+--   apply forall_congr, intro s,
+--   apply imp_congr_ctx h.ne_zero, intro hs,
+--   apply exists_congr, intro n,
+--   sorry
+-- end
+
+end is_equiv
+
+-- lemma trichotomy :
+--   v.is_trivial ∨ v.is_discrete ∨ v.is_non_discrete :=
+-- sorry
+
+end valuation
diff --git a/src/valuation/perfection.lean b/src/valuation/perfection.lean
index bc7617f7..5072ffb5 100644
--- a/src/valuation/perfection.lean
+++ b/src/valuation/perfection.lean
@@ -3,6 +3,7 @@ import field_theory.perfect_closure
 import for_mathlib.nnreal
 
 import valuation.basic
+import valuation.discrete
 
 lemma iterate_frobenius_apply {α : Type*} [monoid α] (p n : ℕ) (a : α) :
   (frobenius α p)^[n] a = a^p^n :=
@@ -84,7 +85,9 @@ end
 end perfection
 
 section
-variables (p : ℕ) [nat.prime p] [char_p R p]
+variables (R) (p : ℕ) [hp : p.prime] [char_p R p]
+
+include hp
 
 def perfection : valuation (perfect_closure R p) nnreal :=
 { to_fun := perfection.f v p,
@@ -101,6 +104,95 @@ def perfection : valuation (perfect_closure R p) nnreal :=
     congr,
   end }
 
+lemma perfection_apply (n : ℕ) (r : R) :
+  v.perfection R p (quot.mk _ ⟨n, r⟩) = v r ^ (p ^ (-n : ℤ) : ℝ) := rfl
+
+@[simp] lemma perfection_of (r : R) :
+  v.perfection R p (perfect_closure.of R p r) = v r :=
+show (v r) ^ _ = v r,
+by simp only [fpow_zero, int.coe_nat_zero, nnreal.rpow_one, neg_zero]
+
+end
+
+namespace perfection
+open filter real
+
+lemma tendsto_pow_zero {x : ℝ} (hx : x ≠ 0) : tendsto (λ ε, x^ε) (nhds (0 : ℝ)) (nhds 1) :=
+begin
+  convert (continuous_rpow_of_ne_zero (λ y, hx) continuous_const continuous_id).continuous_at,
+  simp
 end
 
+-- TODO: rename?
+lemma johan {x ε : ℝ} (hx : 1 < x) (hε : 0 < ε) : ∃ r : ℝ, 0 < r ∧ x^r < 1 + ε :=
+begin
+  have lim := tendsto_pow_zero (by linarith : x ≠ 0),
+  rw metric.tendsto_nhds_nhds at lim,
+  simp only [dist_0_eq_abs, dist_eq, sub_zero] at lim,
+  rcases lim ε hε with ⟨r, rpos, H⟩,
+  use [r/2, by linarith],
+  have : abs (r/2) < r, by rw abs_of_nonneg ; linarith,
+  specialize H this,
+  have : 0 ≤ x ^ (r / 2) - 1,
+  { suffices : 1 ≤ x^(r/2), by linarith,
+    apply one_le_rpow ; linarith },
+  rw abs_of_nonneg this at H,
+  linarith
+end
+
+variables (K : Type*) [discrete_field K] (p : ℕ) [hp : p.prime] [char_p K p]
+include hp
+
+lemma non_discrete (v : valuation K nnreal) (hv : ¬ v.is_trivial) (ε : nnreal) (h : 0 < ε) :
+  ∃ x : perfect_closure K p, 1 < v.perfection K p x ∧ v.perfection K p x < 1 + ε :=
+begin
+  obtain ⟨x, hx⟩ : ∃ x, 1 < v x,
+  { delta is_trivial at hv, push_neg at hv, rcases hv with ⟨x, h₁, h₂⟩,
+    by_cases hx : 1 < v x, { use [x,hx] },
+    use x⁻¹,
+    rw [v.map_inv, ← linear_ordered_structure.inv_lt_inv _ _, inv_inv'', inv_one'],
+    { push_neg at hx, exact lt_of_le_of_ne hx h₂ },
+    { contrapose! h₁, rwa nnreal.inv_eq_zero at h₁ },
+    { exact one_ne_zero } },
+  suffices : ∃ n : ℕ, (v x)^(p^(-n : ℤ) : ℝ) < 1 + ε,
+  { rcases this with ⟨n, hn⟩,
+    refine ⟨quot.mk (perfect_closure.r K p) (n,x), _, hn⟩,
+    change 1 < (v x)^(p^(-n : ℤ) : ℝ),
+    rw nnreal.coe_lt,
+    apply real.one_lt_rpow hx,
+    apply fpow_pos_of_pos,
+    exact_mod_cast hp.pos, },
+  rcases johan hx h with ⟨r, hr, H⟩,
+  -- TODO: the next block is copied from examples/padics, should we extract it?
+  obtain ⟨n, hn⟩ : ∃ n : ℕ, (p : ℝ)^-(n : ℤ) < r,
+    { have hp : (1:ℝ) < p := by exact_mod_cast nat.prime.one_lt ‹_›,
+      obtain ⟨n, hn⟩ : ∃ (n:ℕ), r⁻¹ < p^n := pow_unbounded_of_one_lt r⁻¹ hp,
+      use n,
+      have hp' : (0:ℝ) < p^n,
+      { rw ← fpow_of_nat, apply fpow_pos_of_pos, exact_mod_cast nat.prime.pos ‹_› },
+      rw [inv_lt hr hp', inv_eq_one_div] at hn,
+      rwa [fpow_neg, fpow_of_nat], },
+  use n,
+  transitivity (v x)^r,
+  exact rpow_lt_rpow_of_exponent_lt hx hn,
+  assumption
+end
+
+-- lemma non_discrete' (v : valuation K nnreal) (hv : ¬ v.is_trivial) :
+--   (v.perfection K p).is_non_discrete :=
+-- begin
+--   intros r hr,
+--   by_cases H : v.perfection K p r = 0,
+--   { rcases exists_lt_one_of_not_trivial _ hv with ⟨x, h₁, h₂⟩,
+--     rw H, refine ⟨(perfect_closure.of K p x), _, _⟩,
+--     { contrapose! h₂, rwa [perfection_of, le_zero_iff_eq] at h₂ },
+--     { rwa perfection_of } },
+--   sorry
+--   -- { refine ⟨perfect_field.pth_root 1 r, _, _⟩,
+--   --   {  },
+--   --   {  } }
+-- end
+
+end perfection
+
 end valuation
diff --git a/src/valuation/topology.lean b/src/valuation/topology.lean
index 4c9bcaea..ffaedd5a 100644
--- a/src/valuation/topology.lean
+++ b/src/valuation/topology.lean
@@ -11,7 +11,7 @@ In this file, we define the topology induced by a valuation on a ring.
 local attribute [instance] classical.prop_decidable
 noncomputable theory
 
-local attribute [instance, priority 0] classical.decidable_linear_order
+local attribute [instance, priority 10] classical.decidable_linear_order
 
 open set valuation linear_ordered_structure