Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Hensel's lemma over the p-adic integers #337

Closed
wants to merge 29 commits into from
Closed
Changes from all commits
Commits
Show all changes
29 commits
Select commit Hold shift + click to select a range
4f85f91
feat(data/padics): use has_norm typeclasses for padics
robertylewis Sep 6, 2018
d9f1be1
style(data/padic/padic_integers): remove comment, long line
robertylewis Sep 6, 2018
ba27d2f
feat(data/padics): more scattered lemmas, integers are complete
robertylewis Sep 6, 2018
29f723f
feat(algebra): various helper lemmas, mostly about powers
robertylewis Sep 11, 2018
7587fe2
feat(data/real,analysis/limits): some properties about limits of sequ…
robertylewis Sep 11, 2018
73a0f0d
feat(data/finsupp,data/polynomial): facts about polynomials
robertylewis Sep 11, 2018
237c23f
feat(data/nat): helper lemmas
robertylewis Sep 11, 2018
1b8a2d9
feat(analysis/normed_space,analysis/topology/topological_structures):…
robertylewis Sep 11, 2018
cfad546
feat(data/padics): prove Hensel's lemma
robertylewis Sep 11, 2018
89fa0b7
fix(analysis/normed_space,data/padics): fix mistake in merge; remove …
robertylewis Sep 11, 2018
8e7399d
fix(data/padics/hensel,data/real/cau_seq_filter): missing docstrings
robertylewis Sep 11, 2018
124120f
feat(docs/theories): document padics development
robertylewis Sep 12, 2018
8184c0e
style(data/padics/hensel): polynomials and prime numbers have differe…
robertylewis Sep 12, 2018
a47b547
feat(data/padics): address review comments
robertylewis Sep 17, 2018
82084f6
style(data/polynomial): variable name and comment
robertylewis Sep 17, 2018
713f3c6
feat(data/padics): style, minor refactor
robertylewis Sep 24, 2018
625f76e
feat(data/padics/padic_norm): add division lemma
robertylewis Sep 24, 2018
c199015
feat(data/padics/padic_norm): extra lemmas about padic val and norm
robertylewis Sep 27, 2018
b72cc01
feat(data/real/cau_seq): relate cauchy sequence completeness and filt…
robertylewis Sep 28, 2018
336b6c4
style(analysis/limits,data/real/cau_seq_filter): cleanup
robertylewis Sep 29, 2018
db2c395
remove tactic.find
johoelzl Oct 1, 2018
f37821c
Merge branch 'master' into padic
johoelzl Oct 1, 2018
4719d34
feat(data/padics): use prime typeclass
robertylewis Oct 1, 2018
54cbd88
feat(data/real,data/padics): cauchy_complete typeclass
robertylewis Oct 1, 2018
020924c
fix(data/real,data/padics): remove dead code
robertylewis Oct 1, 2018
7bf76f2
style(data/padics): anonymous instances
robertylewis Oct 2, 2018
01f18f6
fix(data/real,data/padics): fix merge
robertylewis Oct 2, 2018
7a1398e
refactor(data/polynomial): remove analysis import
robertylewis Oct 2, 2018
9c168db
style(analysis/polynomial): unnecessary dsimp
robertylewis Oct 2, 2018
File filter...
Filter file types
Jump to…
Jump to file or symbol
Failed to load files and symbols.
+2,334 −713
Diff settings

Always

Just for now

Copy path View file
@@ -104,7 +104,9 @@ lemma ceil_pos {a : α} : 0 < ⌈a⌉ ↔ 0 < a :=
λ h, have -a < 0, from neg_neg_of_pos h,
neg_pos_of_neg $ lt_of_not_ge $ (not_iff_not_of_iff floor_nonneg).2 $ not_le_of_gt this

lemma ceil_nonneg {q : ℚ} (hq : q 0) : ⌈q⌉ 0 :=
@[simp] theorem ceil_zero : ⌈(0 : α)⌉ = 0 := by simp [ceil]

lemma ceil_nonneg [decidable_rel ((<) : α α Prop)] {q : α} (hq : q 0) : ⌈q⌉ 0 :=
if h : q > 0 then le_of_lt $ ceil_pos.2 h
else
have h' : q = 0, from le_antisymm (le_of_not_lt h) hq,
@@ -233,6 +235,18 @@ begin
← div_lt_iff' (sub_pos.2 h), one_div_eq_inv]
end

theorem exists_nat_one_div_lt {ε : α} (hε : ε > 0) : ∃ n : ℕ, 1 / (n + 1: α) < ε :=
begin
cases archimedean_iff_nat_lt.1 (by apply_instance) (1/ε) with n hn,
existsi n,
apply div_lt_of_mul_lt_of_pos,
{ simp, apply add_pos_of_pos_of_nonneg zero_lt_one, apply nat.cast_nonneg },
{ apply (div_lt_iff' hε).1,
transitivity,
{ exact hn },
{ simp [zero_lt_one] }}
end

include α
@[simp] theorem rat.cast_floor (x : ℚ) :
by haveI := archimedean.floor_ring α; exact ⌊(x:α)⌋ = ⌊x⌋ :=
Copy path View file
@@ -37,7 +37,6 @@ lemma fpow_ne_zero_of_ne_zero {a : α} (ha : a ≠ 0) : ∀ (z : ℤ), fpow a z
| (of_nat n) := pow_ne_zero _ ha
| -[1+n] := one_div_ne_zero $ pow_ne_zero _ ha


@[simp] lemma fpow_zero {a : α} : fpow a 0 = 1 :=
pow_zero _

@@ -58,6 +57,14 @@ lemma zero_fpow : ∀ z : ℤ, z ≠ 0 → fpow (0 : α) z = 0
have h1 : (0 : α) ^ (n+1) = 0, from zero_mul _,
by simp [fpow, h1]

lemma fpow_neg (a : α) : n, fpow a (-n) = 1 / fpow a n
| (of_nat 0) := by simp [of_nat_zero]
| (of_nat (n+1)) := rfl
| -[1+n] := show fpow a (n+1) = 1 / (1 / fpow a (n+1)), by rw one_div_one_div

lemma fpow_sub {a : α} (ha : a 0) (z1 z2 : ℤ) : fpow a (z1 - z2) = fpow a z1 / fpow a z2 :=
by rw [sub_eq_add_neg, fpow_add ha, fpow_neg, ←div_eq_mul_one_div]

end discrete_field_power

section ordered_field_power
@@ -69,6 +76,9 @@ lemma fpow_nonneg_of_nonneg {a : α} (ha : a ≥ 0) : ∀ (z : ℤ), fpow a z
| (of_nat n) := pow_nonneg ha _
| -[1+n] := div_nonneg' zero_le_one $ pow_nonneg ha _

lemma fpow_pos_of_pos {a : α} (ha : a > 0) : (z : ℤ), fpow a z > 0
| (of_nat n) := pow_pos ha _
| -[1+n] := div_pos zero_lt_one $ pow_pos ha _

lemma fpow_le_of_le {x : α} (hx : 1 x) {a b : ℤ} (h : a b) : fpow x a fpow x b :=
begin
@@ -102,4 +112,28 @@ begin
simpa [hfle] using this
end

end ordered_field_power
lemma fpow_le_one_of_nonpos {p : α} (hp : p 1) {z : ℤ} (hz : z 0) : fpow p z 1 :=
calc fpow p z fpow p 0 : fpow_le_of_le hp hz
... = 1 : by simp

lemma fpow_ge_one_of_nonneg {p : α} (hp : p 1) {z : ℤ} (hz : z 0) : fpow p z 1 :=
calc fpow p z fpow p 0 : fpow_le_of_le hp hz
... = 1 : by simp

end ordered_field_power

lemma one_lt_pow {α} [linear_ordered_semiring α] {p : α} (hp : p > 1) : {n : ℕ}, 1 n 1 < p ^ n
| 1 h := by simp; assumption
| (k+2) h :=
begin
rw ←one_mul (1 : α),
apply mul_lt_mul,
{ assumption },
{ apply le_of_lt, simpa using one_lt_pow (nat.le_add_left 1 k)},
{ apply zero_lt_one },
{ apply le_of_lt (lt_trans zero_lt_one hp) }
end

lemma one_lt_fpow {α} [discrete_linear_ordered_field α] {p : α} (hp : p > 1) :
z : ℤ, z > 0 1 < fpow p z
| (int.of_nat n) h := one_lt_pow hp (nat.succ_le_of_lt (int.lt_of_coe_nat_lt_coe_nat h))
Copy path View file
@@ -440,6 +440,38 @@ calc a ^ n = a ^ n * 1 : by simp
(pow_nonneg (le_trans zero_le_one ha) _)
... = a ^ m : by rw [←hk, pow_add]

lemma pow_le_pow_of_le_left {a b : α} (ha : 0 a) (hab : a b) : i : ℕ, a^i b^i
| 0 := by simp
| (k+1) := mul_le_mul hab (pow_le_pow_of_le_left _) (pow_nonneg ha _) (le_trans ha hab)

private lemma pow_lt_pow_of_lt_one_aux {a : α} (h : 0 < a) (ha : a < 1) (i : ℕ) :
k : ℕ, a ^ (i + k + 1) < a ^ i
| 0 := begin simp, rw ←one_mul (a^i), exact mul_lt_mul ha (le_refl _) (pow_pos h _) zero_le_one end
| (k+1) :=
begin
rw ←one_mul (a^i),
apply mul_lt_mul ha _ _ zero_le_one,
{ apply le_of_lt, apply pow_lt_pow_of_lt_one_aux },
{ show 0 < a ^ (i + (k + 1) + 0), apply pow_pos h }
end

private lemma pow_le_pow_of_le_one_aux {a : α} (h : 0 a) (ha : a 1) (i : ℕ) :
k : ℕ, a ^ (i + k) a ^ i
| 0 := by simp
| (k+1) := by rw [←add_assoc, ←one_mul (a^i)];
exact mul_le_mul ha (pow_le_pow_of_le_one_aux _) (pow_nonneg h _) zero_le_one

lemma pow_lt_pow_of_lt_one {a : α} (h : 0 < a) (ha : a < 1)
{i j : ℕ} (hij : i < j) : a ^ j < a ^ i :=
let ⟨k, hk⟩ := nat.exists_eq_add_of_lt hij in
by rw hk; exact pow_lt_pow_of_lt_one_aux h ha _ _

lemma pow_le_pow_of_le_one {a : α} (h : 0 a) (ha : a 1)
{i j : ℕ} (hij : i j) : a ^ j a ^ i :=
let ⟨k, hk⟩ := nat.exists_eq_add_of_le hij in
by rw hk; exact pow_le_pow_of_le_one_aux h ha _ _


end linear_ordered_semiring

theorem pow_two_nonneg [linear_ordered_ring α] (a : α) : 0 a ^ 2 :=
@@ -457,4 +489,10 @@ lemma units_pow_two (u : units ℤ) : u ^ 2 = 1 :=
lemma units_pow_eq_pow_mod_two (u : units ℤ) (n : ℕ) : u ^ n = u ^ (n % 2) :=
by conv {to_lhs, rw ← nat.mod_add_div n 2}; simp [pow_add, pow_mul, units_pow_two]

end int
end int

@[simp] lemma neg_square {α} [ring α] (z : α) : (-z)^2 = z^2 :=
by simp [pow, monoid.pow]

lemma div_sq_cancel {α} [field α] {a : α} (ha : a 0) (b : α) : a^2 * b / a = a * b :=
by rw [pow_two, mul_assoc, mul_div_cancel_left _ ha]
Copy path View file
@@ -81,6 +81,22 @@ lemma one_lt_mul {a b : α} (ha : 1 ≤ a) (hb : 1 < b) : 1 < a * b :=
lemma mul_le_one {a b : α} (ha : a 1) (hb' : 0 b) (hb : b 1) : a * b 1 :=
begin rw ← one_mul (1 : α), apply mul_le_mul; {assumption <|> apply zero_le_one} end

lemma mul_le_iff_le_one_left {a b : α} (hb : b > 0) : a * b b a 1 :=
λ h, le_of_not_lt (mt (lt_mul_iff_one_lt_left hb).2 (not_lt_of_ge h)),
λ h, le_of_not_lt (mt (lt_mul_iff_one_lt_left hb).1 (not_lt_of_ge h)) ⟩

lemma mul_lt_iff_lt_one_left {a b : α} (hb : b > 0) : a * b < b a < 1 :=
λ h, lt_of_not_ge (mt (le_mul_iff_one_le_left hb).2 (not_le_of_gt h)),
λ h, lt_of_not_ge (mt (le_mul_iff_one_le_left hb).1 (not_le_of_gt h)) ⟩

lemma mul_le_iff_le_one_right {a b : α} (hb : b > 0) : b * a b a 1 :=
λ h, le_of_not_lt (mt (lt_mul_iff_one_lt_right hb).2 (not_lt_of_ge h)),
λ h, le_of_not_lt (mt (lt_mul_iff_one_lt_right hb).1 (not_lt_of_ge h)) ⟩

lemma mul_lt_iff_lt_one_right {a b : α} (hb : b > 0) : b * a < b a < 1 :=
λ h, lt_of_not_ge (mt (le_mul_iff_one_le_right hb).2 (not_le_of_gt h)),
λ h, lt_of_not_ge (mt (le_mul_iff_one_le_right hb).1 (not_le_of_gt h)) ⟩

end linear_ordered_semiring

instance linear_ordered_semiring.to_no_top_order {α : Type*} [linear_ordered_semiring α] :
Copy path View file
@@ -134,6 +134,22 @@ by_cases
tendsto_inverse_at_top_nhds_0,
tendsto_cong this $ univ_mem_sets' $ by simp *)

lemma tendsto_coe_iff {f : ℕ ℕ} : tendsto (λ n, (f n : ℝ)) at_top at_top tendsto f at_top at_top :=
λ h, tendsto_infi.2 $ λ i, tendsto_principal.2
(have _, from tendsto_infi.1 h i, by simpa using tendsto_principal.1 this),
λ h, tendsto.comp h tendsto_of_nat_at_top_at_top ⟩

lemma tendsto_pow_at_top_at_top_of_gt_1_nat {k : ℕ} (h : k > 1) : tendsto (λn:ℕ, k ^ n) at_top at_top :=
tendsto_coe_iff.1 $
have hr : (k : ℝ) > 1, from show (k : ℝ) > (1 : ℕ), from nat.cast_lt.2 h,
by simpa using tendsto_pow_at_top_at_top_of_gt_1 hr

lemma tendsto_inverse_at_top_nhds_0_nat : tendsto (λ n : ℕ, (n : ℝ)⁻¹) at_top (nhds 0) :=
tendsto.comp (tendsto_coe_iff.2 tendsto_id) tendsto_inverse_at_top_nhds_0

lemma tendsto_one_div_at_top_nhds_0_nat : tendsto (λ n : ℕ, 1/(n : ℝ)) at_top (nhds 0) :=
by simpa only [inv_eq_one_div] using tendsto_inverse_at_top_nhds_0_nat

lemma sum_geometric' {r : ℝ} (h : r 0) :
{n}, (finset.range n).sum (λi, (r + 1) ^ i) = ((r + 1) ^ n - 1) / r
| 0 := by simp [zero_div]
Copy path View file
@@ -84,6 +84,9 @@ abs_le.2 $ and.intro
lemma dist_norm_norm_le (g h : α) : dist ∥g∥ ∥h∥ ∥g - h∥ :=
abs_norm_sub_norm_le g h

lemma norm_sub_rev (g h : α) : ∥g - h∥ = ∥h - g∥ :=
by rw ←norm_neg; simp

section nnnorm

def nnnorm (a : α) : nnreal := ⟨norm a, norm_nonneg a⟩
@@ -179,6 +182,13 @@ instance normed_ring.to_normed_group [β : normed_ring α] : normed_group α :=
lemma norm_mul {α : Type*} [normed_ring α] (a b : α) : (∥a*b∥) (∥a∥) * (∥b∥) :=
normed_ring.norm_mul _ _

lemma norm_pow {α : Type*} [normed_ring α] (a : α) : {n : ℕ}, n > 0 ∥a^n∥ ∥a∥^n
| 1 h := by simp
| (n+2) h :=
le_trans (norm_mul a (a^(n+1)))
(mul_le_mul (le_refl _)
(norm_pow (nat.succ_pos _)) (norm_nonneg _) (norm_nonneg _))

instance prod.normed_ring [normed_ring α] [normed_ring β] : normed_ring (α × β) :=
{ norm_mul := assume x y,
calc
@@ -192,6 +202,43 @@ instance prod.normed_ring [normed_ring α] [normed_ring β] : normed_ring (α ×
..prod.normed_group }
end normed_ring

instance normed_ring_top_monoid [normed_ring α] : topological_monoid α :=
⟨ continuous_iff_tendsto.2 $ λ x, tendsto_iff_norm_tendsto_zero.2 $
This conversation was marked as resolved by johoelzl

This comment has been minimized.

Copy link
@johoelzl

johoelzl Sep 17, 2018

Collaborator

This should be already available!
Each normed_ring should be a normed_group should be a topological_monoid.

This comment has been minimized.

Copy link
@robertylewis

robertylewis Sep 17, 2018

Author Collaborator

A normed_group is a topological_add_monoid, not a topological_monoid. The topologial_ring instance right below this fails if this isn't here.

This comment has been minimized.

Copy link
@johoelzl

johoelzl Sep 17, 2018

Collaborator

Argh, thanks for the clarification.

have e : α × α, e.fst * e.snd - x.fst * x.snd =
e.fst * e.snd - e.fst * x.snd + (e.fst * x.snd - x.fst * x.snd), by intro; rw sub_add_sub_cancel,
begin
apply squeeze_zero,
{ intro, apply norm_nonneg },
{ simp only [this], intro, apply norm_triangle },
{ rw ←zero_add (0 : ℝ), apply tendsto_add,
{ apply squeeze_zero,
{ intro, apply norm_nonneg },
{ intro t, show ∥t.fst * t.snd - t.fst * x.snd∥ ∥t.fst∥ * ∥t.snd - x.snd∥,
rw ←mul_sub, apply norm_mul },
{ rw ←mul_zero (∥x.fst∥), apply tendsto_mul,
{ apply continuous_iff_tendsto.1,
apply continuous.comp,
{ apply continuous_fst },
{ apply continuous_norm }},
{ apply tendsto_iff_norm_tendsto_zero.1,
apply continuous_iff_tendsto.1,
apply continuous_snd }}},
{ apply squeeze_zero,
{ intro, apply norm_nonneg },
{ intro t, show ∥t.fst * x.snd - x.fst * x.snd∥ ∥t.fst - x.fst∥ * ∥x.snd∥,
rw ←sub_mul, apply norm_mul },
{ rw ←zero_mul (∥x.snd∥), apply tendsto_mul,
{ apply tendsto_iff_norm_tendsto_zero.1,
apply continuous_iff_tendsto.1,
apply continuous_fst },
{ apply tendsto_const_nhds }}}}
end

instance normed_top_ring [normed_ring α] : topological_ring α :=
⟨ continuous_iff_tendsto.2 $ λ x, tendsto_iff_norm_tendsto_zero.2 $
have e : α, -e - -x = -(e - x), by intro; simp,
by simp only [this, norm_neg]; apply lim_norm ⟩

section normed_field

class normed_field (α : Type*) extends has_norm α, discrete_field α, metric_space α :=
@@ -201,6 +248,31 @@ class normed_field (α : Type*) extends has_norm α, discrete_field α, metric_s
instance normed_field.to_normed_ring [i : normed_field α] : normed_ring α :=
{ norm_mul := by finish [i.norm_mul], ..i }

@[simp] lemma norm_one {α : Type*} [normed_field α] : ∥(1 : α)∥ = 1 :=
have ∥(1 : α)∥ * ∥(1 : α)∥ = ∥(1 : α)∥ * 1, by calc
∥(1 : α)∥ * ∥(1 : α)∥ = ∥(1 : α) * (1 : α)∥ : by rw normed_field.norm_mul
... = ∥(1 : α)∥ * 1 : by simp,
eq_of_mul_eq_mul_left (ne_of_gt ((norm_pos_iff _).2 (by simp))) this

@[simp] lemma norm_div {α : Type*} [normed_field α] (a b : α) : ∥a/b∥ = ∥a∥/∥b∥ :=
if hb : b = 0 then by simp [hb] else
begin
apply eq_div_of_mul_eq,
{ apply ne_of_gt, apply (norm_pos_iff _).mpr hb },
{ rw [←normed_field.norm_mul, div_mul_cancel _ hb] }
end

@[simp] lemma norm_inv {α : Type*} [normed_field α] (a : α) : ∥a⁻¹= ∥a∥⁻¹ :=
by simp only [inv_eq_one_div, norm_div, norm_one]

@[simp] lemma normed_field.norm_pow {α : Type*} [normed_field α] (a : α) :
n : ℕ, ∥a^n∥ = ∥a∥^n
| 0 := by simp
| (k+1) := calc
∥a ^ (k + 1)∥ = ∥a*(a^k)∥ : rfl
... = ∥a∥*∥a^k∥ : by rw normed_field.norm_mul
... = ∥a∥ ^ (k + 1) : by rw normed_field.norm_pow; simp [pow, monoid.pow]

instance : normed_field ℝ :=
{ norm := λ x, abs x,
dist_eq := assume x y, rfl,
Copy path View file
@@ -0,0 +1,27 @@
/-
Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Robert Y. Lewis
Analytic facts about polynomials.
-/

import analysis.topology.topological_structures data.polynomial

lemma polynomial.continuous_eval {α} [comm_semiring α] [decidable_eq α] [topological_space α]
[topological_semiring α] (p : polynomial α) : continuous (λ x, p.eval x) :=
begin
apply p.induction,
{ convert continuous_const,
ext, show polynomial.eval x 0 = 0, from rfl },
{ intros a b f haf hb hcts,
simp only [polynomial.eval_add],
refine continuous_add _ hcts,
have : x, finsupp.sum (finsupp.single a b) (λ (e : ℕ) (a : α), a * x ^ e) = b * x ^a,
from λ x, finsupp.sum_single_index (by simp),
convert continuous_mul _ _,
{ ext, apply this },
{ apply_instance },
{ apply continuous_const },
{ apply continuous_pow }}
end
@@ -42,6 +42,10 @@ lemma continuous_mul [topological_space β] {f : β → α} {g : β → α}
continuous (λx, f x * g x) :=
(hf.prod_mk hg).comp continuous_mul'

lemma continuous_pow : n : ℕ, continuous (λ a : α, a ^ n)
| 0 := by simpa using continuous_const
| (k+1) := show continuous (λ (a : α), a * a ^ k), from continuous_mul continuous_id (continuous_pow _)

lemma tendsto_mul' {a b : α} : tendsto (λp:α×α, p.fst * p.snd) (nhds (a, b)) (nhds (a * b)) :=
continuous_iff_tendsto.mp (topological_monoid.continuous_mul α) (a, b)

Copy path View file
@@ -391,6 +391,11 @@ finset.sum_add_distrib
{h : α β γ} : f.sum (λa b, - h a b) = - f.sum h :=
finset.sum_hom (@has_neg.neg γ _) neg_zero (assume a b, neg_add _ _)

@[simp] lemma sum_sub [add_comm_monoid β] [add_comm_group γ] {f : α ₀ β}
{h₁ h₂ : α β γ} :
f.sum (λa b, h₁ a b - h₂ a b) = f.sum h₁ - f.sum h₂ :=
by rw [sub_eq_add_neg, ←sum_neg, ←sum_add]; refl

@[simp] lemma sum_single [add_comm_monoid β] {f : α ₀ β} :
f.sum single = f :=
have a:α, f.sum (λa' b, ite (a' = a) b 0) =
Copy path View file
@@ -582,22 +582,25 @@ lemma dvd_nat_abs_of_of_nat_dvd {a : ℕ} : ∀ {z : ℤ} (haz : ↑a ∣ z), a
have haz' : (↑a:ℤ) ∣ (↑(k+1):ℤ), from dvd_of_dvd_neg haz,
int.coe_nat_dvd.1 haz'

lemma pow_div_of_le_of_pow_div_int {p m n : ℕ} {k : ℤ} (hmn : m n) (hdiv : ↑(p ^ n) ∣ k) :
lemma pow_dvd_of_le_of_pow_dvd {p m n : ℕ} {k : ℤ} (hmn : m n) (hdiv : ↑(p ^ n) ∣ k) :
↑(p ^ m) ∣ k :=
begin
induction k,
{ apply int.coe_nat_dvd.2,
apply pow_div_of_le_of_pow_div hmn,
apply pow_dvd_of_le_of_pow_dvd hmn,
apply int.coe_nat_dvd.1 hdiv },
{ change -[1+k] with -(↑(k+1) : ℤ),
apply dvd_neg_of_dvd,
apply int.coe_nat_dvd.2,
apply pow_div_of_le_of_pow_div hmn,
apply pow_dvd_of_le_of_pow_dvd hmn,
apply int.coe_nat_dvd.1,
apply dvd_of_dvd_neg,
exact hdiv }
end

lemma dvd_of_pow_dvd {p k : ℕ} {m : ℤ} (hk : 1 k) (hpk : ↑(p^k) ∣ m) : ↑p ∣ m :=
by rw ←nat.pow_one p; exact pow_dvd_of_le_of_pow_dvd hk hpk

/- / and ordering -/

protected theorem div_mul_le (a : ℤ) {b : ℤ} (H : b 0) : a / b * b a :=
Oops, something went wrong.
ProTip! Use n and p to navigate between commits in a pull request.
You can’t perform that action at this time.