# Zulip Chat Archive

## Stream: maths

### Topic: golfing challenge

#### Johan Commelin (May 02 2020 at 17:03):

This shouldn't be so hard/long/slow...

```
import ring_theory.polynomial
namespace polynomial
/-- The formal derivative of polynomials, as additive homomorphism. -/
noncomputable def derivative_hom (R : Type*) [comm_semiring R] : polynomial R →+ polynomial R :=
{ to_fun := derivative,
map_zero' := derivative_zero,
map_add' := λ p q, derivative_add }
@[simp] lemma derivative_neg {R : Type*} [comm_ring R] (f : polynomial R) :
derivative (-f) = -derivative f :=
(derivative_hom R).map_neg f
@[simp] lemma derivative_sub {R : Type*} [comm_ring R] (f g : polynomial R) :
derivative (f - g) = derivative f - derivative g :=
(derivative_hom R).map_sub f g
lemma is_coprime_of_is_root_of_eval_derivative_ne_zero {R : Type*} [field R]
(f : polynomial R) (r : R) (hf : f.is_root r) (hf' : f.derivative.eval r ≠ 0) :
ideal.is_coprime (X - C r : polynomial R) (f /ₘ (X - C r)) :=
begin
rw ← mul_div_by_monic_eq_iff_is_root at hf,
rw ← hf at hf',
simp only [eval_C, eval_X, add_zero, derivative_X, derivative_mul, one_mul, zero_mul,
eval_sub, sub_zero, ne.def, derivative_sub, eval_add, eval_mul, derivative_C, sub_self] at hf',
apply is_coprime_of_dvd,
{ push_neg, left, assume eqz,
apply_fun polynomial.degree at eqz,
rw polynomial.degree_X_sub_C at eqz,
exact option.no_confusion eqz },
{ rintros a h1 h2 ⟨b, hab⟩ H,
have : irreducible (X - C r),
{ apply polynomial.irreducible_of_degree_eq_one, exact polynomial.degree_X_sub_C _ },
rcases (this.is_unit_or_is_unit hab) with ha|⟨b,rfl⟩,
{ exact h1 ha },
apply hf',
show is_root _ _,
rw ← dvd_iff_is_root,
refine dvd_trans ⟨↑b⁻¹, _⟩ H,
rw [hab, units.mul_inv_cancel_right] }
end
end polynomial
```

#### Alex J. Best (May 02 2020 at 18:15):

Probably this can be golfed more, but heres a slightly different proof (I think?)

```
lemma is_coprime_of_is_root_of_eval_derivative_ne_zero {R : Type*} [field R]
(f : polynomial R) (r : R) (hf : f.is_root r) (hf' : f.derivative.eval r ≠ 0) :
ideal.is_coprime (X - C r : polynomial R) (f /ₘ (X - C r)) :=
begin
have aa : (X - C r) * (f /ₘ (X - C r)) = f - (f %ₘ (X - C r)) := begin
rw [eq_sub_iff_add_eq, ← eq_sub_iff_add_eq', mod_by_monic_eq_sub_mul_div],
exact monic_X_sub_C r,
end,
apply_fun derivative at aa,
simp only [derivative_X, derivative_mul, one_mul, sub_zero, derivative_sub, mod_by_monic_X_sub_C_eq_C_eval, derivative_C] at aa,
refine or.resolve_left (dvd_or_coprime (X - C r) (f /ₘ (X - C r)) (irreducible_of_degree_eq_one (polynomial.degree_X_sub_C r))) _,
intro,
apply hf',
have : (X - C r) ∣ derivative f := aa ▸ (dvd_add a (dvd.intro (derivative (f /ₘ (X - C r))) rfl)),
rw [← dvd_iff_mod_by_monic_eq_zero (monic_X_sub_C _), mod_by_monic_X_sub_C_eq_C_eval] at this,
apply_fun coeff at this,
convert congr_fun this 0,
rw [coeff_C_zero],
end
```

#### Johan Commelin (May 02 2020 at 20:42):

Thanks... it's certainly shorter than what I had.

#### Johan Commelin (May 09 2020 at 12:25):

Feel free to turn this into a kata.

```
import data.nat.choose
-- Generalise this to arbitrary property that is respected by addition/multiplication:
-- example applications: sum_pos, sum_neg, ... others?
lemma dvd_sum {α : Type*} {R : Type*} [comm_ring R]
(s : finset α) (f : α → R) (b : R) (H : ∀ a ∈ s, b ∣ f a) :
b ∣ s.sum f :=
begin
let t := s,
replace H : ∀ a ∈ t, b ∣ f a := H,
have hs : s ⊆ t := finset.subset.refl s,
revert hs,
classical,
apply finset.induction_on s, {simp},
intros a s' ha IH hs',
rw finset.insert_subset at hs',
cases hs' with has hs',
simp [*, dvd_add]
end
lemma coe_nat_dvd {α : Type*} [comm_ring α] (m n : ℕ) (h : m ∣ n) :
(m : α) ∣ n :=
by { rcases h with ⟨k, rfl⟩, refine ⟨k, by norm_cast⟩ }
lemma dvd_sub_pow_of_dvd_sub (R : Type*) [comm_ring R] (p : ℕ) [hp : fact p.prime]
(a b : R) (h : (p : R) ∣ a - b) (k : ℕ) :
(p^(k+1) : R) ∣ a^(p^k) - b^(p^k) :=
begin
induction k with k ih, { simpa using h }, clear h,
simp only [nat.succ_eq_add_one],
rcases ih with ⟨c, hc⟩,
rw sub_eq_iff_eq_add' at hc,
replace hc := congr_arg (λ x, x^p) hc,
dsimp only at hc,
rw [← pow_mul, add_pow, finset.sum_range_succ, nat.choose_self, nat.cast_one, mul_one,
nat.sub_self, pow_zero, mul_one] at hc,
conv { congr, skip, rw [nat.pow_succ] },
simp only [nat.pow_eq_pow] at hc,
rw [hc, pow_mul, add_sub_cancel'], clear hc a,
apply dvd_sum,
intros i hi,
rw finset.mem_range at hi,
rw mul_pow,
conv { congr, skip, congr, congr, skip, rw mul_comm },
repeat { rw mul_assoc, apply dvd_mul_of_dvd_right }, clear c b,
norm_cast,
apply coe_nat_dvd,
by_cases H : i = 0,
{ subst H,
suffices : p ^ (k + 1 + 1) ∣ (p ^ (k + 1)) ^ p, by simpa,
rw ← nat.pow_mul,
apply nat.pow_dvd_pow,
refine le_trans (add_le_add_left' $ le_add_left $ le_refl _ : k + 1 + 1 ≤ k + 1 + (k + 1)) _,
refine le_trans (le_of_eq _) (nat.mul_le_mul_left (k+1) $ (hp.two_le : 2 ≤ p)),
rw mul_two },
have i_pos := nat.pos_of_ne_zero H, clear H,
rw nat.pow_succ,
apply mul_dvd_mul,
{ generalize H : (p^(k+1)) = b,
have := nat.sub_pos_of_lt hi,
conv {congr, rw ← nat.pow_one b},
apply nat.pow_dvd_pow,
exact this },
exact nat.prime.dvd_choose i_pos hi ‹_›
end
```

#### Johan Commelin (May 09 2020 at 12:25):

Currently it takes so long on my machine that I'm worried codewars wouldn't accept it.

#### Reid Barton (May 09 2020 at 12:26):

Johan Commelin said:

Feel free to turn this into a

~~kata~~mathlib PR.

#### Johan Commelin (May 09 2020 at 12:26):

Only after it's fast enough to be a kata

#### Chris Hughes (May 09 2020 at 12:43):

The generalization of the first theorem is `is_add_submonoid.sum_mem`

. Whether that's a good way to state it I don't know.

#### Johan Commelin (May 09 2020 at 12:44):

But it might be a good way to prove it.

#### Johan Commelin (May 09 2020 at 12:45):

On the other hand, the other suggestions don't really follow from `sum_mem`

, I guess. Things like `sum_pos`

and `sum_neg`

#### Johan Commelin (May 09 2020 at 12:46):

Well, they do, but I don't think the relevant submonoids have been set up.

#### Chris Hughes (May 09 2020 at 13:19):

`sum_pos`

and `sum_neg`

actually need `is_add_subsemigroup.sum_mem_of_ne_empty`

which doesn't exist.

#### Johan Commelin (May 09 2020 at 13:20):

`sum_nonpos`

and `sum_nonneg`

...

#### Kenny Lau (May 09 2020 at 14:07):

```
import data.nat.choose algebra.geom_sum ring_theory.ideals
-- Generalise this to arbitrary property that is respected by addition/multiplication:
-- example applications: sum_pos, sum_neg, ... others?
lemma dvd_sum {α : Type*} {R : Type*} [comm_ring R]
(s : finset α) (f : α → R) (b : R) (H : ∀ a ∈ s, b ∣ f a) :
b ∣ s.sum f :=
begin
classical, revert H,
apply finset.induction_on s,
{ intros, exact dvd_zero b, },
intros a s has ih H,
rw finset.forall_mem_insert at H,
rw finset.sum_insert has,
exact dvd_add H.1 (ih H.2)
end
lemma coe_nat_dvd {α : Type*} [comm_ring α] (m n : ℕ) (h : m ∣ n) :
(m : α) ∣ n :=
by { rcases h with ⟨k, rfl⟩, refine ⟨k, by norm_cast⟩ }
instance {α : Type*} [comm_ring α] (I : ideal α) : is_ring_hom (ideal.quotient.mk I) :=
(ideal.quotient.mk_hom I).is_ring_hom
lemma mk_eq_mk_hom {α : Type*} [comm_ring α] (I : ideal α) (x : α) :
ideal.quotient.mk I x = ideal.quotient.mk_hom I x :=
rfl
theorem ring_hom.map_geom_series₂ {α β : Type*} [comm_ring α] [comm_ring β] (x y : α) (n : ℕ)
(f : α →+* β) : f (geom_series₂ x y n) = geom_series₂ (f x) (f y) n :=
by { rw [geom_series₂_def, geom_series₂_def, ← finset.sum_hom _ f],
simp_rw [f.map_mul, f.map_pow] }
theorem geom_series₂_self {α : Type*} [comm_ring α] (x : α) (n : ℕ) :
geom_series₂ x x n = n * x ^ (n-1) :=
calc (finset.range n).sum (λ i, x ^ i * x ^ (n - 1 - i))
= (finset.range n).sum (λ i, x ^ (i + (n - 1 - i))) : by simp_rw [← pow_add]
... = (finset.range n).sum (λ i, x ^ (n - 1)) : finset.sum_congr rfl
(λ i hi, congr_arg _ $ nat.add_sub_cancel' $ nat.le_pred_of_lt $ finset.mem_range.1 hi)
... = add_monoid.smul (finset.range n).card (x ^ (n - 1)) : finset.sum_const _
... = n * x ^ (n - 1) : by rw [finset.card_range, add_monoid.smul_eq_mul]
lemma dvd_sub_pow_of_dvd_sub (R : Type*) [comm_ring R] (p : ℕ) [hp : fact p.prime]
(a b : R) (h : (p : R) ∣ a - b) (k : ℕ) :
(p^(k+1) : R) ∣ a^(p^k) - b^(p^k) :=
begin
induction k with k ih,
{ rwa [pow_one, nat.pow_zero, pow_one, pow_one] },
rw [nat.pow_succ, pow_mul, pow_mul, ← geom_sum₂_mul, pow_succ],
refine mul_dvd_mul _ ih,
rw [← ideal.mem_span_singleton, ← ideal.quotient.eq, mk_eq_mk_hom, mk_eq_mk_hom] at h,
rw [← ideal.mem_span_singleton, ← ideal.quotient.eq_zero_iff_mem, mk_eq_mk_hom,
ring_hom.map_geom_series₂, ring_hom.map_pow, ring_hom.map_pow, h, geom_series₂_self,
← ring_hom.map_pow, ← ring_hom.map_pow, ← add_monoid.smul_eq_mul],
erw [← (ideal.quotient.mk_hom (ideal.span ({p} : set R))).to_add_monoid_hom.map_smul,
ideal.quotient.eq_zero_iff_mem],
rw add_monoid.smul_eq_mul,
exact ideal.mul_mem_right _ (ideal.mem_span_singleton.2 $ dvd_refl (p : R))
end
```

#### Kenny Lau (May 09 2020 at 14:08):

@Johan Commelin the trick is to use `geom_series\2`

and quotient ring

#### Johan Commelin (May 09 2020 at 14:12):

@Kenny Lau Sounds good. Thanks! Wanna make a PR?

#### Kenny Lau (May 09 2020 at 14:12):

go ahead

#### Johan Commelin (May 09 2020 at 14:32):

@Kenny Lau Golfed further:

```
lemma dvd_sub_pow_of_dvd_sub (R : Type*) [comm_ring R] (p : ℕ) [hp : fact p.prime]
(a b : R) (h : (p : R) ∣ a - b) (k : ℕ) :
(p^(k+1) : R) ∣ a^(p^k) - b^(p^k) :=
begin
induction k with k ih,
{ rwa [pow_one, nat.pow_zero, pow_one, pow_one] },
rw [nat.pow_succ, pow_mul, pow_mul, ← geom_sum₂_mul, pow_succ],
refine mul_dvd_mul _ ih,
have : (p : R) ∈ ideal.span ({p} : set R), { rw ideal.mem_span_singleton },
rw [← ideal.quotient.eq_zero_iff_mem, mk_eq_mk_hom, ring_hom.map_nat_cast] at this,
rw [← ideal.mem_span_singleton, ← ideal.quotient.eq, mk_eq_mk_hom, mk_eq_mk_hom] at h,
rw [← ideal.mem_span_singleton, ← ideal.quotient.eq_zero_iff_mem, mk_eq_mk_hom,
ring_hom.map_geom_series₂, ring_hom.map_pow, ring_hom.map_pow, h, geom_series₂_self,
this, zero_mul],
end
```

#### Kenny Lau (May 09 2020 at 14:33):

@Johan Commelin aha, you applied the quotient philosophy even more

#### Kevin Buzzard (May 09 2020 at 15:03):

Wow, from a monster it's now at de Bruijn index 1!

#### Johan Commelin (May 09 2020 at 15:11):

#### Johan Commelin (May 09 2020 at 16:57):

Unexpected side effect: the proof doesn't use that `p`

is prime (-;

#### Johan Commelin (May 09 2020 at 16:58):

Maybe not so unexpected after all. But that hypothesis certainly existed in my mental copy of this lemma (-;

#### Johan Commelin (May 09 2020 at 16:58):

Linters are good.

#### Kenny Lau (May 09 2020 at 17:03):

wow that's unexpected

#### Mario Carneiro (May 09 2020 at 17:03):

it's probably because you called the variable `p`

#### Johan Commelin (May 09 2020 at 17:04):

It's called `n`

now (-;

#### Reid Barton (May 09 2020 at 17:07):

I sort of think it should still be called `p`

#### Reid Barton (May 09 2020 at 17:07):

I had no idea this was true for `p`

not prime and I would certainly expect to see `p`

in the theorem statement

#### Johan Commelin (May 09 2020 at 17:07):

Oops... I didn't update the theorem name...

#### Johan Commelin (May 09 2020 at 17:09):

@Reid Barton You can prove the special case, if you want :grinning_face_with_smiling_eyes:

#### Reid Barton (May 09 2020 at 17:10):

I don't need the special case, I just want the theorem statement to read as expected, with the `prime p`

hypothesis mysteriously absent.

#### Johan Commelin (May 09 2020 at 17:15):

Sure, was only joking

#### Kevin Buzzard (May 09 2020 at 17:24):

Yeah I like that style, it's kind of an in joke

#### Kevin Buzzard (May 09 2020 at 17:25):

For 2 you can beat this result, 2^(k+2) divides the 2^kth power if k>=1.

#### Johan Commelin (May 09 2020 at 17:26):

And does this get used somewhere?

#### Kevin Buzzard (May 09 2020 at 17:26):

And the pair (1,5) show that this is tight for all k>=1

#### Kevin Buzzard (May 09 2020 at 17:26):

Analogous to the pair (1,p+1) showing its tight for odd primes

#### Johan Commelin (May 09 2020 at 17:27):

You mean for arbitrary `p ≥ 3`

?

#### Johan Commelin (May 09 2020 at 17:27):

For `p = 1`

you can do even better than for `p = 2`

!!!

#### Kevin Buzzard (May 09 2020 at 17:27):

Yes you can use it to demonstrate that 1+p resp 5 have large multiplicative orders mod p^n, and determine their order precisely

#### Johan Commelin (May 09 2020 at 17:28):

And is this fact about `5`

used somewhere?

#### Kevin Buzzard (May 09 2020 at 17:28):

This gives you the structure theorem for the units of Z/p^nZ and then by CRT the structure of the units in Z/NZ

#### Johan Commelin (May 09 2020 at 17:28):

Aah, I see

#### Kevin Buzzard (May 09 2020 at 17:29):

Yes it tells you that the units in Z/32 have an element of order 8 and with that and the elements +-17 you know the structure of the group modulo the structure theorem

#### Kevin Buzzard (May 09 2020 at 17:29):

Which you can probably prove by hand here

#### Johan Commelin (May 09 2020 at 17:29):

`dec_trivial`

?

#### Johan Commelin (May 09 2020 at 17:30):

Lol, just kidding

#### Kevin Buzzard (May 09 2020 at 17:30):

If only

#### Johan Commelin (May 09 2020 at 17:30):

But were you aware that this lemma doesn't need the primality assumption?

#### Kevin Buzzard (May 09 2020 at 17:30):

It's `come_on_lean`

you need

#### Kevin Buzzard (May 09 2020 at 17:30):

No I didn't know

#### Johan Commelin (May 09 2020 at 17:30):

Would that give you a speed up for the structure theorem?

#### Kevin Buzzard (May 09 2020 at 17:30):

But everything I said needed it

#### Johan Commelin (May 09 2020 at 17:30):

Ok, I see

#### Johan Commelin (May 09 2020 at 17:31):

Well, we can make those tightness bounds into an issue for later

#### David Wärn (May 09 2020 at 17:42):

I think this is made more precise by the "Lifting the Exponent lemma", i.e. "$v_p(a^n - b^n) = v_p(a-b) + v_p(n)$ for p odd prime with p dividing $a-b$ but not a or b"

#### Johan Commelin (May 09 2020 at 17:44):

But that needs the primality assumption...

#### David Wärn (May 09 2020 at 17:47):

Probably one direction does, yes

#### David Wärn (May 09 2020 at 17:48):

Or maybe both... Not sure

Last updated: May 19 2021 at 02:10 UTC