## 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,

@[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
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',
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,
rcases ih with ⟨c, 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],
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?

#### 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!

#2640

#### 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

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

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

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

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