Zulip Chat Archive

Stream: maths

Topic: Cyclotomic polynomials


view this post on Zulip Riccardo Brasca (Sep 17 2020 at 15:16):

Hi, I am (slowly) starting to work with cyclotomic polynomials. At the moment I have defined them as the minimal polynomial of exp(2piI/n). In this way the irreducibility and rationality of the coefficients are of course for free, the main result being about the degree (I didn't check yet what is in mathlib to prove that the coefficients are integers). Do you see any specific reason to follow the other way? I mean, defining them as something like Prod (X - zeta) for zeta a primitive root of unity and then prove the rest. I randomly chose my approach so I am ready to change my mind :)

view this post on Zulip Johan Commelin (Sep 17 2020 at 15:45):

@Kenny Lau @Kevin Buzzard :up:

view this post on Zulip Kenny Lau (Sep 17 2020 at 15:52):

@Riccardo Brasca the main lemma is to show that dnΦd=Xn1\prod_{d \mid n} \Phi_d = X^n - 1

view this post on Zulip Riccardo Brasca (Sep 17 2020 at 15:57):

@Kenny Lau Yes, of course. My question was if you see any reason to prefer one of the following definitions for Ψd\Psi_d:
1) minimal polynomial of exp(2πi/n)\exp(2\pi i/n)
2) ζμ(Xζ)\prod_{{\zeta} \in \mu^\ast} (X - \zeta), where μ\mu^\ast is the set of primitive root of unity.

view this post on Zulip Kenny Lau (Sep 17 2020 at 15:57):

I prefer 1

view this post on Zulip Kenny Lau (Sep 17 2020 at 15:57):

because it's in Z[x] automatically

view this post on Zulip Kenny Lau (Sep 17 2020 at 15:58):

then you prove that its coercion to C[x] is 2

view this post on Zulip Johan Commelin (Sep 17 2020 at 15:58):

Defining integral polynomials by first defining them as rational polynomials and then proving that the coefficients are integral is a bit of a pain. If you can avoid it, I would recommend that.

view this post on Zulip Riccardo Brasca (Sep 17 2020 at 15:59):

Perfect! It is what I have already written, for the same reason (almost, I am struggling with some stupid identity of complex numbers that does not want to be proved...)

view this post on Zulip Adam Topaz (Sep 17 2020 at 15:59):

Aren't minimal polynomials (for algebraic things over Q\mathbf{Q}) defined as generators of ideals in Q[X]\mathbf{Q}[X] and hence as polynomials over Q\mathbf{Q}?

view this post on Zulip Adam Topaz (Sep 17 2020 at 16:01):

Or is there something in mathlib that tells you the minimal polynomial over Z\mathbf{Z} assuming the element is integral?

view this post on Zulip Riccardo Brasca (Sep 17 2020 at 16:01):

@Johan Commelin I do not see any way of defining them directly as elements of Z[X]\mathbf{Z}[X], unless mathlib knows about algebraic integers.

view this post on Zulip Riccardo Brasca (Sep 17 2020 at 16:01):

@Adam Topaz I will check it.

view this post on Zulip Johan Commelin (Sep 17 2020 at 16:21):

@Riccardo Brasca I think I might start with something like

import data.polynomial.div

open_locale classical big_operators
noncomputable theory

variables (R : Type*) [comm_ring R]

namespace polynomial

noncomputable
def cyclotomic :   polynomial R
| 0 := 0
| 1 := X - 1
| n@(k + 2) := (X ^ n - 1) /  i : {i : fin n // i  n}, have (i : ) < n := i.1.2,
                                cyclotomic i

end polynomial

view this post on Zulip Johan Commelin (Sep 17 2020 at 16:22):

This is very minimal. The definition is as crazy as it is, because Lean needs to know that the inductive definition is well-founded.

view this post on Zulip Johan Commelin (Sep 17 2020 at 16:23):

So the first thing we should now do, is show that we can just take the product that we want, without the crazy have statement, and the subtype of fin n.

view this post on Zulip Riccardo Brasca (Sep 17 2020 at 16:23):

I will think about it, now what I wrote is rather different, since it uses the minimal polynomial of a primitive root of unity...

view this post on Zulip Johan Commelin (Sep 17 2020 at 16:23):

After that, we should prove things about cyclotomic \C n (that e ^ (2 * pi / n) is a root, etc).

view this post on Zulip Johan Commelin (Sep 17 2020 at 16:24):

Then show that the product formula holds over \C. And deduce it for \Z, since \Z \to \C is injective.

view this post on Zulip Riccardo Brasca (Sep 17 2020 at 16:26):

By the way, I am stuck with the very stupid fact that exp(2πi/n)n=1\exp(2 \pi i/n)^n = 1. This is of course only my fault, but I can't finish this proof (I tried some basic tactic and I can do a long proof, but I am sure there must be something very quick)?

import analysis.special_functions.trigonometric

lemma stupid (n : ) : n  0  (complex.exp (2*real.pi*complex.I/n))^n = 1 :=
begin
  intro,
  rw complex.exp_nat_mul,
  apply complex.exp_eq_one_iff.2,
  use 1,
end

view this post on Zulip Johan Commelin (Sep 17 2020 at 16:26):

Actually, the definition can just be

def cyclotomic :   polynomial R
| n := (X ^ n - 1) /  i : {i : fin n // (i : )  n}, have (i : ) < n := i.1.2,
                                cyclotomic i

view this post on Zulip Kenny Lau (Sep 17 2020 at 16:30):

@Riccardo Brasca you can prove that it's integral over Z

view this post on Zulip Johan Commelin (Sep 17 2020 at 16:32):

lemma stupid (n : ) (h : n  0) : (complex.exp (2*real.pi*complex.I/n))^n = 1 :=
begin
  rw [ complex.exp_nat_mul,
      mul_div_cancel' _ (show (n : )  0, by exact_mod_cast h),
      complex.exp_eq_one_iff],
  use 1,
  simp,
end

view this post on Zulip Johan Commelin (Sep 17 2020 at 16:32):

@Riccardo Brasca :up:

view this post on Zulip Riccardo Brasca (Sep 17 2020 at 16:34):

@Johan Commelin Thank you very much! I guess it takes some time to become used to write proofs this way...

view this post on Zulip Johan Commelin (Sep 17 2020 at 16:34):

You were pretty close already

view this post on Zulip Johan Commelin (Sep 17 2020 at 16:37):

@Riccardo Brasca Leaving of from your start, the following three lines also close the goal:

  have : (n : )  0, by assumption_mod_cast,
  field_simp [this],
  ring,

view this post on Zulip Riccardo Brasca (Sep 17 2020 at 16:37):

Yes, I thought that someting like ring would have done the job, but maybe it doesn't like multiplicative inverse (it's called ring and not field...)

view this post on Zulip Johan Commelin (Sep 17 2020 at 16:37):

First, you tell Lean that n is nonzero, viewed as complex number.

view this post on Zulip Riccardo Brasca (Sep 17 2020 at 16:37):

Ah, there is field_simp!

view this post on Zulip Johan Commelin (Sep 17 2020 at 16:37):

Then field_simp can use that fact to cancel the division.

view this post on Zulip Johan Commelin (Sep 17 2020 at 16:37):

After that, the goal is almost trivial, but because we are lazy, we use ring to close it (-;

view this post on Zulip Heather Macbeth (Sep 17 2020 at 16:39):

I think that

lemma also_stupid : complex.exp (2 * real.pi * complex.I) = 1

should be added to the library, also.

view this post on Zulip Riccardo Brasca (Sep 17 2020 at 16:41):

Yes, I think that at least for psychological reasons we should explicitly have eπi+1=0e^{\pi i } + 1 = 0.

view this post on Zulip Heather Macbeth (Sep 17 2020 at 16:43):

That one does exist! docs#complex.exp_pi_mul_I

view this post on Zulip Heather Macbeth (Sep 17 2020 at 16:44):

(As of last week -- #3746 :smiley: )

view this post on Zulip Johan Commelin (Sep 17 2020 at 17:18):

I guess we'll need to prove

lemma X_pow_sub_one_eq_prod (n : ) :
  (X ^ n - 1 : polynomial ) =
   i in range n, (X - C (complex.exp (2 * real.pi * complex.I * i / n))) :=
begin
  sorry
end

view this post on Zulip Riccardo Brasca (Sep 17 2020 at 17:20):

Another very stupid problem: how do I prove that Xn10X^n - 1 \neq 0? Sorry for the question, but I had a look at the proof that X0X \neq 0 and it is quite difficult to understand.

view this post on Zulip Johan Commelin (Sep 17 2020 at 17:21):

This might be an intermediate step

lemma roots_X_pow_sub_one (n : ) :
  roots (X ^ n - 1 : polynomial ) =
  multiset.map (λ (i : ), complex.exp (2 * real.pi * complex.I * i / n)) (multiset.range n) :=
begin
  sorry
end

view this post on Zulip Kenny Lau (Sep 17 2020 at 17:21):

@Riccardo Brasca it isn't true if n = 0! ;)

view this post on Zulip Johan Commelin (Sep 17 2020 at 17:21):

Riccardo Brasca said:

Another very stupid problem: how do I prove that Xn10X^n - 1 \neq 0? Sorry for the question, but I had a look at the proof that X0X \neq 0 and it is quite difficult to understand.

Of course you will need to use somewhere that 1 \ne 0

view this post on Zulip Johan Commelin (Sep 17 2020 at 17:22):

Right, and n \ne 0

view this post on Zulip Riccardo Brasca (Sep 17 2020 at 17:22):

Yes, that's not the problem n0n \neq 0 is in the assumptions!

view this post on Zulip Johan Commelin (Sep 17 2020 at 17:23):

It would be good if we had a tactic that could do those

view this post on Zulip Johan Commelin (Sep 17 2020 at 17:24):

Note that there is a lemma X_pow_sub_C_ne_zero

view this post on Zulip Johan Commelin (Sep 17 2020 at 17:24):

Together with C_1, that will make the proof easy.

view this post on Zulip Riccardo Brasca (Sep 17 2020 at 17:25):

OK, I have to improve my skills in finding what already is in mathlib :)

view this post on Zulip Riccardo Brasca (Sep 17 2020 at 17:35):

I finished the definition of Ψd\Psi_d as minimal polynomial over Q\mathbf{Q} of exp(2πi/d))\exp(2\pi i /d)) (so this is not the same definition proposed by @Johan Commelin but it is the one I have in my mind). In particular ΨdQ[X]\Psi_d \in \mathbf{Q}[X] is irreducible. Tomorrow I will try to prove that it is actually in Z[X]\mathbf{Z}[X] and see if I can prove the formula for Xd1X^d - 1. Thank you for all your comments!!

view this post on Zulip Reid Barton (Sep 17 2020 at 17:39):

Johan Commelin said:

It would be good if we had a tactic that could do those

This probably mainly needs a test suite

view this post on Zulip Johan Commelin (Sep 17 2020 at 17:44):

lemma roots_X_pow_sub_one (n : ) :
  roots (X ^ n - 1 : polynomial ) =
  multiset.map (λ (i : ), complex.exp (2 * real.pi * complex.I * i / n)) (multiset.range n) :=
begin
  rw [ C_1],
  by_cases hn : n = 0,
  { simp only [hn, div_zero, multiset.card_zero, roots_zero, nat.cast_zero, multiset.map_const,
      multiset.range_zero, ring_hom.map_one, multiset.repeat_zero, pow_zero, sub_self] },
  have H := X_pow_sub_C_ne_zero (nat.pos_of_ne_zero hn) (1 : ),
  symmetry,
  rw eq_iff_le_not_lt,
  split,
  { rw multiset.le_iff_subset,
    { intro x,
      simp only [multiset.mem_map, multiset.mem_range, mem_roots H,
        is_root, eval_sub, eval_pow, eval_X, eval_C, sub_eq_zero],
      rintro i, hi, rfl,
      rw [ complex.exp_nat_mul, complex.exp_eq_one_iff],
      use i,
      have : (n : )  0, by assumption_mod_cast,
      field_simp [this],
      ring, },
    { apply multiset.nodup_map_on _ (multiset.nodup_range n),
      sorry } },
  { intro h,
    replace h := multiset.card_lt_of_lt h,
    rw [multiset.card_map, multiset.card_range,  not_le] at h,
    apply h,
    exact card_roots_X_pow_sub_C (nat.pos_of_ne_zero hn) (1 : ) }
end

@Riccardo Brasca

view this post on Zulip Johan Commelin (Sep 17 2020 at 17:45):

Still has one sorry left.

view this post on Zulip Johan Commelin (Sep 17 2020 at 17:57):

Do we know anything like: two monic polynomials over \C are equal if they have the same roots?

view this post on Zulip Kevin Buzzard (Sep 17 2020 at 17:58):

What is the type of roots f?

view this post on Zulip Adam Topaz (Sep 17 2020 at 17:58):

multiset right?

view this post on Zulip Johan Commelin (Sep 17 2020 at 17:59):

eq_prod_roots_of_splits

view this post on Zulip Adam Topaz (Sep 17 2020 at 17:59):

Otherwise why would anyone ever use multiset.map?

view this post on Zulip Riccardo Brasca (Sep 17 2020 at 17:59):

@Johan Commelin Thank you. My code looks A LOT less sophisticated than your :D In any case I think I can prove that Xn1=dnΨdX^n - 1 = \prod_{d | n} \Psi_d in a week or so.

view this post on Zulip Johan Commelin (Sep 17 2020 at 18:06):

We should probably also decide whether the 0th cyclotomic polynomial is X ^ 0 - 1 or the empty product...

view this post on Zulip Adam Topaz (Sep 17 2020 at 18:08):

roots 0 seems to be defined as \varnothing.

view this post on Zulip Kenny Lau (Sep 17 2020 at 18:09):

I don't understand why you can't make it in Z[X] using docs#minimal_polynomial

view this post on Zulip Adam Topaz (Sep 17 2020 at 18:10):

Kenny Lau said:

I don't understand why you can't make it in Z[X] using docs#minimal_polynomial

Adam Topaz said:

Or is there something in mathlib that tells you the minimal polynomial over Z\mathbf{Z} assuming the element is integral?

Cool. I didn't know that existed.

view this post on Zulip Riccardo Brasca (Sep 17 2020 at 18:11):

Yes, integral coefficients is not a problem.

view this post on Zulip Alex J. Best (Sep 17 2020 at 18:11):

Johan Commelin said:

We should probably also decide whether the 0th cyclotomic polynomial is X ^ 0 - 1 or the empty product...

Clearly it should be a degree 2 polynomial so that deg(Φn)=ϕ(n)\deg (\Phi_n) = \phi(n) holds with https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Arithmetic.20Functions/near/209952965

view this post on Zulip Adam Topaz (Sep 17 2020 at 18:12):

Clearly φ(0)=\varphi(0) = -\infty since that's the degree of the zero polynomial.

view this post on Zulip Adam Topaz (Sep 17 2020 at 18:18):

I think Φ0=1\Phi_0 = 1 is a sensible choice.

view this post on Zulip Johan Commelin (Sep 17 2020 at 19:31):

In the X-adic topology i0,i0Φi\prod_{i \mid 0, i \ne 0} \Phi_i converges to -1. Does that tell us anything about Φ0\Phi_0?

view this post on Zulip Adam Topaz (Sep 17 2020 at 19:31):

I was thinking of the fact that the limit of nn in Z^\widehat{\mathbf{Z}} is 00 with respect to divisibility.

view this post on Zulip Johan Commelin (Sep 17 2020 at 19:36):

Right, maybe ϕ(n)\phi(n) counts not the number of units in Z/nZ\mathbb{Z}/n\mathbb{Z}, but in Z^/nZ^\hat\mathbb{Z}/n\hat\mathbb{Z}.

view this post on Zulip Johan Commelin (Sep 17 2020 at 19:38):

So then ϕ(0)\phi(0) should be infinity, and the degree of Φ0\Phi_0 should be ... hmm, it never really matches up.

view this post on Zulip Adam Topaz (Sep 17 2020 at 19:38):

Ha. Do you know this fun paper by Lenstra about profinite Fibonacci numbers?

view this post on Zulip Johan Commelin (Sep 17 2020 at 19:38):

Nope...

view this post on Zulip Adam Topaz (Sep 17 2020 at 19:39):

http://www.math.leidenuniv.nl/~hwl/papers/fibo.pdf

view this post on Zulip Adam Topaz (Sep 17 2020 at 19:40):

φ\varphi can be extended to functions on Z^\widehat{\mathbf{Z}} in the way you said, and the fact that it's multiplicative boils down to the isomorphism

Z^pZp.\widehat{\mathbf{Z}} \cong \prod_p \mathbf{Z}_p.

view this post on Zulip Adam Topaz (Sep 17 2020 at 19:41):

Or maybe it should be extended to supernatural numbers.

view this post on Zulip Joseph Myers (Sep 17 2020 at 19:48):

Kenny Lau said:

Riccardo Brasca the main lemma is to show that dnΦd=Xn1\prod_{d \mid n} \Phi_d = X^n - 1

There's also the corresponding statement in the other direction, but I don't see any sign of Möbius inversion in mathlib.

view this post on Zulip Johan Commelin (Sep 17 2020 at 19:49):

Nope, I guess it is popping up higher and higher on our "most-wanted" list (-;

view this post on Zulip Alex J. Best (Sep 17 2020 at 20:02):

See also https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Perfect.20Numbers/near/201455256 for some discussion on moebius stuff

view this post on Zulip Riccardo Brasca (Sep 17 2020 at 23:08):

I am really confused by polynomials... how do I prove (polynomial.X ^ n - 1).monic? It should be done by polynomial.monic_X_pow_sub but I do not see how. Here of course n>0n > 0.

view this post on Zulip Riccardo Brasca (Sep 17 2020 at 23:43):

OK, I figured out a (very ugly) proof :)

view this post on Zulip Kenny Lau (Sep 18 2020 at 07:05):

import data.polynomial

universe u

variables {R : Type u} [ring R]

open polynomial

lemma nat.with_bot.lt_succ_iff {m : with_bot } {n : } : m < n.succ  m  n :=
begin
  cases m,
  { exact iff_of_true (with_bot.bot_lt_coe _) bot_le },
  { rw [with_bot.some_eq_coe, with_bot.coe_lt_coe, with_bot.coe_le_coe, nat.lt_succ_iff] }
end

lemma monic_X_pow_sub' {p : polynomial R} {n : } (hpn : p.degree < n) : (X ^ n - p).monic :=
begin
  cases n,
  { rw [with_bot.coe_zero, nat.with_bot.lt_zero_iff, degree_eq_bot] at hpn,
    rw [hpn, pow_zero, sub_zero],
    exact monic_one },
  { rw nat.with_bot.lt_succ_iff at hpn,
    exact monic_X_pow_sub hpn }
end

theorem monic_X_pow_sub_one {n : } (hn : 0 < n) : (X ^ n - 1 : polynomial R).monic :=
begin
  refine monic_X_pow_sub' (lt_of_le_of_lt degree_one_le _),
  rwa [ with_bot.coe_zero, with_bot.coe_lt_coe]
end

view this post on Zulip Johan Commelin (Sep 18 2020 at 07:12):

Why the prime on monic_X_pow_sub'. Was there already a lemma monic_X_pow_sub? What could it say, if not the statement you proved?

view this post on Zulip Kenny Lau (Sep 18 2020 at 07:13):

monic_X_pow_sub : ?M_3.degree  ↑?M_4  (X ^ (?M_4 + 1) - ?M_3).monic

view this post on Zulip Riccardo Brasca (Sep 18 2020 at 13:44):

Do we have some form of Gauss lemma in mathlib? I see that people are working on it for UFD, but I need it just for Z\mathbf{Z} (to prove that Φd\Phi_d is irreducible over Q\mathbf{Q}).

view this post on Zulip Johan Commelin (Sep 18 2020 at 15:20):

Nope, I don't think so

view this post on Zulip Aaron Anderson (Nov 01 2020 at 02:36):

#4861 should have the version of Gauss's Lemma that you want.

view this post on Zulip Aaron Anderson (Nov 01 2020 at 02:37):

What else do we need for Cyclotomic polynomials, Moebius inversion?

view this post on Zulip Thomas Browning (Nov 01 2020 at 02:38):

At some point we might need them when working with cyclotomic fields

view this post on Zulip Thomas Browning (Nov 01 2020 at 02:39):

Or maybe I have your question the wrong way around

view this post on Zulip Aaron Anderson (Nov 01 2020 at 02:59):

Anyway, @Riccardo Brasca, let me know if there are any other prereqs you need for cyclotomic polynomials.

view this post on Zulip Riccardo Brasca (Nov 01 2020 at 17:48):

That's a great news! I am almost ready to submit a first PR with all the basic results (integral coefficients and the product formula). With Gauss lemma I will be able to prove irreducibility. I do not need Moebius inversion to prove this :)

view this post on Zulip Aaron Anderson (Nov 01 2020 at 17:58):

Ok, sweet. Hopefully Gauss’s lemma merges by the time your second PR is ready, and I’ll try to get Moebius inversion ready for a third one on the degree formula.

view this post on Zulip Riccardo Brasca (Nov 01 2020 at 18:15):

You mean that the degree is φ n? I already have it... with my definition (product of X - \zeta, for \zeta a primitive root of unity in \C) it follows from results about primitive roots that already are in mathlib.

view this post on Zulip Kevin Buzzard (Nov 01 2020 at 19:19):

There's a fairly cheap proof that there are infinitely many primes congruent to 1 mod NN using cyclotomic polynomials. That would be a cool thing to have.

view this post on Zulip Riccardo Brasca (Nov 01 2020 at 19:36):

I will try to do it.

view this post on Zulip Johan Commelin (Nov 06 2020 at 16:04):

#4914 has been merged :octopus: Congrats @Riccardo Brasca :clink:

view this post on Zulip Riccardo Brasca (Nov 06 2020 at 17:13):

Thank you! Just for fun I am trying to compute explicitly cyclotomic 105 ℤ... we will see if it is doable.

view this post on Zulip Kevin Buzzard (Nov 06 2020 at 17:48):

The famous counterexample!

view this post on Zulip Kevin Buzzard (Nov 06 2020 at 17:49):

Lean 3 is not designed to do computations, and polynomials are noncomputable, and complex numbers are noncomputable, so I am not at all optimistic that this will succeed :-)

view this post on Zulip Riccardo Brasca (Nov 06 2020 at 18:22):

Yes, of course that's not what Lean is designed for, but still we can prove stuff like a ^ 2 - b ^ 2 = (a + b) * (a - b) in any commutative ring, so we can do some computations. I am curious to see how far one can go using ring.

view this post on Zulip Filippo A. E. Nuccio (Nov 06 2020 at 19:18):

Good luck :wink:

view this post on Zulip Mario Carneiro (Nov 06 2020 at 19:20):

@Riccardo Brasca What's the computation method here? I can help if you actually want to do this

view this post on Zulip Johan Commelin (Nov 06 2020 at 19:25):

https://en.wikipedia.org/wiki/Cyclotomic_polynomial#Fundamental_tools

view this post on Zulip Johan Commelin (Nov 06 2020 at 19:25):

But we don't have Mobius yet...

view this post on Zulip Johan Commelin (Nov 06 2020 at 19:26):

I guess we can try working with polynomial division. But I'm not sure if norm_num is good for something like that.

view this post on Zulip Johan Commelin (Nov 06 2020 at 19:26):

Maybe a specific "plugin" could do it?

view this post on Zulip Mario Carneiro (Nov 06 2020 at 19:26):

a plugin could do it

view this post on Zulip Mario Carneiro (Nov 06 2020 at 19:26):

but actually we don't need polynomial division since it's exact. Just prove the multiplication

view this post on Zulip Mario Carneiro (Nov 06 2020 at 19:27):

Especially if you allow the user to supply lots of hints this can be done pretty efficiently without too much extra stuff

view this post on Zulip Mario Carneiro (Nov 06 2020 at 19:29):

I think the relevant theorem for computing cyclotomic 105 is Φnp(x)=Φn(xp)/Φn(x)\Phi_{np}(x)=\Phi_n(x^p)/\Phi_n(x) where pp does not divide nn

view this post on Zulip Mario Carneiro (Nov 06 2020 at 19:29):

is this proven?

view this post on Zulip Johan Commelin (Nov 06 2020 at 19:30):

Nope, almost no rules are proven (in mathlib). I don't know if Riccardo has more stuff on a branch

view this post on Zulip Johan Commelin (Nov 06 2020 at 19:32):

Mario Carneiro said:

but actually we don't need polynomial division since it's exact. Just prove the multiplication

This only works if you already know the answer. Which we do in this case... but still

view this post on Zulip Kevin Buzzard (Nov 06 2020 at 19:34):

Mario Carneiro said:

I think the relevant theorem for computing cyclotomic 105 is Φnp(x)=Φn(xp)/Φn(x)\Phi_{np}(x)=\Phi_n(x^p)/\Phi_n(x) where pp does not divide nn

Another alternative is dnΦd(x)=xn1\prod_{d\mid n}\Phi_d(x)=x^n-1 giving a recursive procedure for computing them -- and I believe that this _is_ in mathlib.

view this post on Zulip Mario Carneiro (Nov 06 2020 at 19:35):

that sounds far less efficient though, since you would have to calculate all the polynomials leading up to it

view this post on Zulip Mario Carneiro (Nov 06 2020 at 19:35):

although I guess it's fine if you intend to make a table with all of them

view this post on Zulip Mario Carneiro (Nov 06 2020 at 19:36):

wikipedia seems to make an exception to the table for 105

view this post on Zulip Kevin Buzzard (Nov 06 2020 at 20:07):

105 is the first counterexample to the conjecture "all coefficients are 0 or +-1" IIRC

view this post on Zulip Riccardo Brasca (Nov 06 2020 at 20:07):

No, that is not proven. What I am doing now is using that if PP satisfies P(in,i<nΦi)=Xn1P \cdot (\prod_{i|n , i < n}\Phi_i) = X^n -1 then P=ΦnP = \Phi_n. It is bit painful to explicitly write down the set of divisors, but it seems to it is doable.

view this post on Zulip Riccardo Brasca (Nov 06 2020 at 20:08):

Yes, that's why I am trying with 105... I do not want to make a list until there :)

view this post on Zulip Riccardo Brasca (Nov 06 2020 at 20:09):

Ah, I see that you predicted my strategy :)

view this post on Zulip Reid Barton (Nov 06 2020 at 20:15):

are you trying to prove that 105 is a counterexample, or that it's the first one?

view this post on Zulip Riccardo Brasca (Nov 06 2020 at 20:20):

I am just curious to see if I am able to give the explicit formula for Φ105\Phi_{105}. It is just for fun :D

view this post on Zulip Riccardo Brasca (Nov 06 2020 at 20:27):

For example, is there a simple way to automatize the fact that {a, b, c}.card = 3 (with the correct assumptions on a b c)?

view this post on Zulip Riccardo Brasca (Nov 06 2020 at 20:28):

I mean, it's not difficult, but it becomes quickly quite annoying if we have four or more elements..

view this post on Zulip Mario Carneiro (Nov 06 2020 at 20:32):

You should use nat.factors, which is a list

view this post on Zulip Mario Carneiro (Nov 06 2020 at 20:32):

you can get lean to prove [a, b, c].length = 3 pretty easily

view this post on Zulip Riccardo Brasca (Nov 07 2020 at 01:39):

If you don't mind wasting RAM and CPU time I have proof of

lemma cyclotomic_105 : cyclotomic 105  =
  1 + X + X ^ 2 - X ^ 5 - X ^ 6 - 2 * X ^ 7 - X ^ 8 - X ^ 9 + X ^ 12 + X ^ 13 + X ^ 14 + X ^ 15
  + X ^ 16 + X ^ 17 - X ^ 20 - X ^ 22 - X ^ 24 - X ^ 26 - X ^ 28 + X ^ 31 + X ^ 32 + X ^ 33 +
  X ^ 34 + X ^ 35 + X ^ 36 - X ^ 39 - X ^ 40 - 2 * X ^ 41 - X ^ 42 - X ^ 43 + X ^ 46 + X ^ 47 +
  X ^ 48

:rolling_on_the_floor_laughing:

view this post on Zulip Mario Carneiro (Nov 07 2020 at 02:21):

what's the proof?

view this post on Zulip Johan Commelin (Nov 07 2020 at 06:58):

how many lines is the proof? is it "readable"?

view this post on Zulip Kevin Buzzard (Nov 07 2020 at 07:21):

Well done! Getting lean to calculate is hard work!

view this post on Zulip Riccardo Brasca (Nov 07 2020 at 11:43):

You can read the proof here (remove the last ring if you want to save your RAM)

https://webusers.imj-prg.fr/~riccardo.brasca/files/cyclotomic105.lean

I think it is long but very readable.

Essentially the lemma that allows the computation of cyclotomic polynomial is compute_cyclotomic at the very beginning. Because of this I have to explicitly compute the set of (proper) divisors of 105 = 3 * 5 * 7.

At first I tried to be general, working with two distinct primes p and q. To prove that (p * q).nat.divisors = {1, p, q, p * q} I use arithmetic_function.sigma 0 n to prove that it has four elements (there must be a simpler way...) and then I prove by hand that {1, p, q, p * q} has four elements and it is included in (p * q).nat.divisors = {1, p, q, p * q}. This is in the sections preliminaries and semiprime.
Then I do the same for three primes p q w, in the section three_primes. Again everything is trivial but I got lazy in proving that {1, p, q, w, p * q, p * w, q * w, p * q * w} has eight elements and I didn't do it in general (all the rest is done).

I can now start computing cyclotomic polynomials, in section cyclotomic. For one prime it is easy (not that, funny enough, the lemma polynomial.cyclotomic_of_prime that is the only one that deserves to be in mathlib, it's not used at the end). Also for two primes there are no problems, I used norm_num as least as possible, only to prove that 3, 5, 7 are primes and pairwise disjoints.

The ugliest part is in section one_hundred_five, where I used norm_num to prove stuff like 15 ≠ 21, that can be done in general. I prove, very ugly, by hand, that {1, 3, 5, 7, 15, 21, 35} has seven elements . This requires proving, by hand, stuff like not_mem_15 that say 15 ∉ ({1, 3, 5, 7}. For some reasons finset.card_insert_of_not_mem inserts the new element at "the end" of the set, while finset.prod_insert does it "at the beginning" at the set, so I also wrote not_mem_15' (I didn't spent too much time thinking about why this happens).

In any case, I have nat.proper_divisors (105) = {1, 3, 5, 7, 15, 21, 35} and so in the proof of cyclotomic_105 I can use inset.prod_insert not_mem_?' several times. Given that I already have computed all the other cyclotomic polynomials, at the end I just let ring doing the job.

view this post on Zulip Johan Commelin (Nov 07 2020 at 12:36):

@Mario Carneiro Certainly it shouldn't be hard for norm_num to compute nat.proper_divisors (105) = {1, 3, 5, 7, 15, 21, 35}, right?

view this post on Zulip Reid Barton (Nov 07 2020 at 12:52):

Isn't there also some recurrence relation which could be used to split off a single prime at a time? then you wouldn't need to deal with all this finset stuff

view this post on Zulip Riccardo Brasca (Nov 07 2020 at 12:52):

When I started thinking about it it was really strange, and very different from how we (humans) think about it. For example, I have no idea how to prove that finset.range 105 = {0, 1, ..., 104} (the dots are just for readability, in Lean I would have written all the numbers) except by showing that the set on the right is included in the one on the left and then comparing the cardinalities. And still, showing that {0, 1, ..., 104} by hand it is super long. Probably, as Kevin said, this is not what Lean is designed for.

view this post on Zulip Riccardo Brasca (Nov 07 2020 at 12:54):

@Reid Barton This is possible, I looked for it but I didn't find anything useful about nat.divisors. If you meant for cyclotomic polynomials, at the moment my strategy is the only one available in mathlib.

view this post on Zulip Reid Barton (Nov 07 2020 at 12:59):

Wikipedia says that Φnp(X)=Φn(Xp)/Φn(X)\Phi_{np}(X) = \Phi_n(X^p) / \Phi_n(X) for pp prime and not dividing nn. Then you could prove a theorem like the one you have, that says that if P(X)Φn(X)=Φn(Xp)P(X) \cdot \Phi_n(X) = \Phi_n(X^p) then P=ΦnpP = \Phi_{np}, and apply it twice to get from 3 to 15 to 105 (say).

view this post on Zulip Reid Barton (Nov 07 2020 at 12:59):

Is your comment about nat.divisors related to this?

view this post on Zulip Reid Barton (Nov 07 2020 at 13:01):

Regarding computation: the vision is that the library of tactics you need for these things just doesn't happen to exist yet. By analogy, you'd probably also have a hard time proving prime 101 without tactic support.

view this post on Zulip Riccardo Brasca (Nov 07 2020 at 13:04):

@Reid Barton Yes, of course this is entirely possible, and more interesting. I just wrote the basic of cyclotomic polynomials and I think I will work on something that for me is more interesting (like the irreducibility). I was just curious to see if this computation was doable in Lean, and I realized that the problems are not where I was expecting them: ring is very powerful and has no problem in doing long calculations, but I struggled in proving things like that {1,2,3,4,5,6} has six elements.

view this post on Zulip Riccardo Brasca (Nov 07 2020 at 13:05):

As you say the reason is clear, both computation and stuff like that require some tactic to do the work for us, and we have better tactic for computations, simply because they are needed far more often than tactic to handle explicit numbers.

view this post on Zulip Reid Barton (Nov 07 2020 at 13:11):

This one is true by rfl as it happens: example : ({1,2,3,4,5,6} : finset ℕ).card = 6 := rfl

view this post on Zulip Reid Barton (Nov 07 2020 at 13:12):

although you wouldn't want to use this method if the numbers were a lot larger

view this post on Zulip Reid Barton (Nov 07 2020 at 13:12):

and it might be better to avoid using this on general principles

view this post on Zulip Reid Barton (Nov 07 2020 at 13:18):

otherwise, it's clearly in the range of problems that simp and norm_num could solve if they teamed up, but I can't figure out how to make them do it

view this post on Zulip Riccardo Brasca (Nov 07 2020 at 13:19):

I didn't even thought about trying rfl... why it works ? It must do some checks, for example to avoid ({1, 1} : finset ℕ).card = 2.

view this post on Zulip Reid Barton (Nov 07 2020 at 13:21):

Basically because the relevant parts of finset are constructive given a decidable_eq instance for the type involved ( in this case)

view this post on Zulip Reid Barton (Nov 07 2020 at 13:24):

so reducing ({1,2,3,4,5,6} : finset ℕ).card does basically the computation that you wrote out, except that in order to test whether elements of are equal, it uses the decidable_eq ℕ instance, which is defined by recursion

view this post on Zulip Riccardo Brasca (Nov 07 2020 at 13:27):

Aahh, it's a matter of decidable_eq!

view this post on Zulip Kevin Buzzard (Nov 07 2020 at 13:32):

Looks like it:

import tactic

inductive foo
| X : foo
| Y : foo

open foo

example : ({X, Y} : finset foo).card = 2 := rfl -- doesn't even compile

@[derive decidable_eq] inductive bar
| A : bar
| B : bar

open bar

example : ({A, B} : finset bar).card = 2 := rfl -- works fine

view this post on Zulip Reid Barton (Nov 07 2020 at 13:33):

So of course we would also like to be able to prove ({1,2,3,4,5,6} : finset ℝ).card = 6 and we need a new strategy for this one.

view this post on Zulip Kevin Buzzard (Nov 07 2020 at 13:33):

Because finset is constructive finite sets, you can't even make {X,Y} because Lean doesn't know an algorithm for figuring out if X=Y so it can't insert X into {Y} whilst keeping track of everything. Of course you can make an algorithm -- that's what @[derive decidable_eq] does.

view this post on Zulip Kevin Buzzard (Nov 07 2020 at 13:35):

The mathematician's approach:

import tactic

open_locale classical

inductive foo
| X : foo
| Y : foo

open foo

example : ({X, Y} : finset foo).card = 2 := rfl -- statement compiles but proof fails

I say "of course there's an algorithm for deciding equality, because there's an algorithm for deciding any true-false statement" and then I can formalise the statement but the proof fails because there isn't actually an algorithm for figuring out if X=Y.

view this post on Zulip Kevin Buzzard (Nov 07 2020 at 13:37):

The problem with making a general algorithm for counting the size of finite sets is that no "dumb" algorithm will be able to compute the size of {n1n2,π2/6}\{\sum_{n\geq1}n^{-2},\pi^2/6\}; one has to prove a theorem first to compute the size of this set.

view this post on Zulip Kevin Buzzard (Nov 07 2020 at 13:38):

But for things within norm_nums capability, one can do something. Not at all sure how easy it would be to automate though!

view this post on Zulip Reid Barton (Nov 07 2020 at 13:39):

In the case {1,2,3,4,5,6}, since we already know all the numbers are different, we can manually write something like

import data.finset
import data.real.basic

example : ({1,2,3,4,5,6} : finset ).card = 6 :=
begin
  repeat { rw finset.card_insert_of_not_mem },
  rw finset.card_singleton,
  all_goals
  { try { repeat { rw finset.mem_insert } },
    rw finset.mem_singleton,
    norm_num },
end

view this post on Zulip Reid Barton (Nov 07 2020 at 13:39):

because we know that finset.card_insert_of_not_mem is the right lemma to apply every time

view this post on Zulip Reid Barton (Nov 07 2020 at 13:41):

but if the input was something like {1,2,3,4,5,1}, then we would need to start with finset.card_insert_of_mem instead

view this post on Zulip Reid Barton (Nov 07 2020 at 13:43):

and this is where the pieces we have at the moment don't quite fit together right--simp doesn't know which lemma to apply because only norm_num knows how to verify the side conditions of the lemmas, but in the original formula, norm_num can't make any progress either

view this post on Zulip Reid Barton (Nov 07 2020 at 13:44):

But you could probably fix this by instead using a lemma like (s.insert x).card = (if x \in s then 0 else 1) + s.card

view this post on Zulip Riccardo Brasca (Nov 07 2020 at 13:44):

Your code is better than mine, but that's essentially what I did, prove by hand that any element is a new element.

view this post on Zulip Riccardo Brasca (Nov 07 2020 at 14:10):

Now the code is quite shorter... and it enters in Zulip :)

import number_theory.arithmetic_function
import ring_theory.polynomial.cyclotomic

open_locale classical big_operators

open polynomial

lemma compute_cyclotomic {R : Type*} [comm_ring R] [nontrivial R] {n : } (hpos: 0 < n)
  (P : polynomial R) :
  P * ( i in nat.proper_divisors n, polynomial.cyclotomic i R) = X ^ n - 1  cyclotomic n R = P :=
begin
  intro hP,
  have prod_monic : ( i in nat.proper_divisors n, cyclotomic i R).monic,
  { apply monic_prod_of_monic,
    intros i hi,
    exact cyclotomic.monic i R },
  rw [@cyclotomic_eq_X_pow_sub_one_div R _ _ _ hpos, (div_mod_by_monic_unique P 0 prod_monic _).1],
  split,
  { rw [zero_add, mul_comm],
    exact hP },
  rw [degree_zero, bot_lt_iff_ne_bot],
  intro h,
  exact monic.ne_zero prod_monic (degree_eq_bot.1 h)
end

lemma card_nat_divisors (n : ) : (n.divisors).card = nat.arithmetic_function.sigma 0 n :=
by simp

lemma proper_divisors_card (n : ) (hpos : 0 < n) :
  (nat.proper_divisors n).card = (nat.divisors n).card - 1 :=
begin
  apply nat.succ.inj,
  have hcard : (nat.divisors n).card = nat.succ (nat.proper_divisors n).card,
  { rw [nat.divisors_eq_proper_divisors_insert_self_of_pos hpos],
    { simp only [true_and, not_lt, nat.mem_proper_divisors, dvd_refl,
    finset.card_insert_of_not_mem] } },
  rw [hcard, nat.pred_eq_sub_one, nat.succ_pred_eq_of_pos],
  apply finset.card_pos.2,
  use 1,
  simp only [ne_of_gt hpos, ne.def, not_false_iff, and_self, nat.mem_divisors, is_unit.dvd,
  nat.is_unit_iff]
end

lemma lt_of_prod_lt_one {a b : } (ha : 1 < a) (hb : 0 < b) : b < a * b :=
begin
  nth_rewrite 0 ←@one_mul  _ b,
  exact mul_lt_mul ha (le_of_eq (refl b)) hb (nat.zero_le a)
end

lemma not_mem_singleton {a b : } (hdiff : a  b) : a  ({b} : finset ) :=
begin
  intro h,
  replace h := (finset.mem_singleton .1 h),
  exact hdiff h
end

lemma not_mem_two {a b c: } (hdiffab : a  b) (hdiffac : a  c) : a  ({b, c} : finset ) :=
begin
  intro h,
  simp only [finset.mem_insert, finset.mem_singleton] at h,
  cases h,
  { exact hdiffab h },
  { exact hdiffac h }
end

lemma card_of_ne {a b : } (hdiff : a  b) : ({a, b} : finset ).card = 2 :=
begin
  have card_eq := finset.card_insert_of_not_mem (not_mem_singleton hdiff),
  rw [finset.card_singleton, one_add_one_eq_two ] at card_eq,
  exact card_eq
end

lemma card_of_ne_of_ne {a b c : } (hdiffab : a  b) (hdiffac : a  c) (hdiffbc : b  c) :
  ({a, b, c} : finset ).card = 3 :=
begin
  have card_eq := finset.card_insert_of_not_mem (not_mem_two hdiffab hdiffac),
  rw [card_of_ne hdiffbc] at card_eq,
  exact card_eq
end

lemma divisors_prime_card {p : } (hp : nat.prime p) : (nat.divisors p).card = 2 :=
begin
  rw [nat.divisors_eq_proper_divisors_insert_self_of_pos (nat.prime.pos hp),
  nat.prime.proper_divisors hp],
  exact card_of_ne (nat.prime.ne_one hp),
end

lemma divisors_semiprime_card {p q : } (hp : nat.prime p) (hq : nat.prime q)
  (hdiff : p  q) : (nat.divisors (p * q)).card = 4 :=
begin
  have fact : nat.arithmetic_function.sigma 0 (p * q) = (nat.arithmetic_function.sigma 0 p) *
  nat.arithmetic_function.sigma 0 q,
  { rw [nat.arithmetic_function.is_multiplicative.map_mul_of_coprime
  nat.arithmetic_function.is_multiplicative_sigma ((nat.coprime_primes hp hq).2 hdiff)] },
  rw [card_nat_divisors, fact, card_nat_divisors, card_nat_divisors, divisors_prime_card hp,
  divisors_prime_card hq],
  ring
end

lemma proper_divisors_semiprime_card {p q : } (hp : nat.prime p) (hq : nat.prime q)
  (hdiff : p  q) : (nat.proper_divisors (p * q)).card = 3 :=
begin
  rw proper_divisors_card _ ,
  { rw divisors_semiprime_card hp hq hdiff },
  simp only [hp.pos, hq.pos, zero_lt_mul_right]
end

lemma proper_divisors_semiprime_supset {p q : } (hp : nat.prime p) (hq : nat.prime q)
  (hdiff : p  q) : {1, p, q}  nat.proper_divisors (p * q) :=
begin
  rw finset.subset_iff,
  intros x hx,
  simp only [finset.mem_insert, finset.mem_singleton] at hx,
  rcases hx with hx1 | hxp | hxq,
  { rw [hx1, nat.mem_proper_divisors],
    split,
    { use p * q,
      rw one_mul },
    exact one_lt_mul (le_of_lt (nat.prime.one_lt hp)) (nat.prime.one_lt hq) },
  { rw [hxp, nat.mem_proper_divisors],
    split,
    { use q },
    rw [mul_comm],
    exact lt_of_prod_lt_one (nat.prime.one_lt hq) hp.pos },
  { rw [hxq, nat.mem_proper_divisors],
    split,
    { use p,
      rw mul_comm },
    exact lt_of_prod_lt_one (nat.prime.one_lt hp) hq.pos }
end

lemma proper_divisors_semiprime {p q : } (hp : nat.prime p) (hq : nat.prime q)
  (hdiff : p  q) : nat.proper_divisors (p * q) = {1, p, q} :=
begin
  symmetry,
  apply finset.eq_of_subset_of_card_le,
  { exact proper_divisors_semiprime_supset hp hq hdiff },
  rw [proper_divisors_semiprime_card hp hq hdiff, card_of_ne_of_ne _ _ hdiff],
  { exact (nat.prime.ne_one hp).symm },
  { exact (nat.prime.ne_one hq).symm }
end

lemma coprime_of_prod_primes {p q w : } (hp : nat.prime p) (hq : nat.prime q) (hw : nat.prime w)
  (hdiffpq : p  q) (hdiffpw : p  w) (hdiffqw : q  w) : nat.coprime p (q * w) :=
begin
  apply or.resolve_right (nat.coprime_or_dvd_of_prime hp (q * w)),
  intro h,
  replace h := (nat.prime.dvd_mul hp).1 h,
  cases h,
  { exact hdiffpq ((nat.prime_dvd_prime_iff_eq hp hq).1 h) },
  { exact hdiffpw ((nat.prime_dvd_prime_iff_eq hp hw).1 h) }
end

lemma divisors_three_primes_card {p q w : } (hp : nat.prime p) (hq : nat.prime q)
  (hw : nat.prime w) (hdiffpq : p  q) (hdiffpw : p  w) (hdiffqw : q  w) :
  (nat.divisors (p * (q * w))).card = 8 :=
begin
  have fact : nat.arithmetic_function.sigma 0 (p * (q * w)) = (nat.arithmetic_function.sigma 0 p) *
  nat.arithmetic_function.sigma 0 (q * w),
  { rw [nat.arithmetic_function.is_multiplicative.map_mul_of_coprime
    nat.arithmetic_function.is_multiplicative_sigma
    (coprime_of_prod_primes hp hq hw hdiffpq hdiffpw hdiffqw)] },
  rw [card_nat_divisors, fact, card_nat_divisors, card_nat_divisors,
  divisors_semiprime_card hq hw hdiffqw, divisors_prime_card hp],
  ring
end

lemma proper_divisors_three_primes_card {p q w : } (hp : nat.prime p) (hq : nat.prime q)
  (hw : nat.prime w) (hdiffpq : p  q) (hdiffpw : p  w) (hdiffqw : q  w) :
  (nat.proper_divisors (p * (q * w))).card = 7 :=
begin
  rw proper_divisors_card _ ,
  { rw divisors_three_primes_card hp hq hw hdiffpq hdiffpw hdiffqw },
  simp only [hp.pos, hq.pos, hw.pos, zero_lt_mul_right]
end

lemma prime_3 : nat.prime 3 := by norm_num

lemma prime_5 : nat.prime 5 := by norm_num

lemma prime_7 : nat.prime 7 := by norm_num

lemma cyclotomic_3 : cyclotomic 3  = 1 + X + X ^ 2 :=
begin
  apply @compute_cyclotomic  _ _ 3 (nat.prime.pos prime_3),
  rw nat.prime.proper_divisors prime_3,
  simp only [finset.prod_singleton, cyclotomic_one],
  ring
end

lemma cyclotomic_5 : cyclotomic 5  = 1 + X + X ^ 2 + X ^ 3 + X ^ 4 :=
begin
  apply @compute_cyclotomic  _ _ 5 (nat.prime.pos prime_5),
  rw nat.prime.proper_divisors prime_5,
  simp only [finset.prod_singleton, cyclotomic_one],
  ring
end

lemma cyclotomic_7 : cyclotomic 7  = 1 + X + X ^ 2 + X ^ 3 + X ^ 4 + X ^ 5 + X ^ 6 :=
begin
  apply @compute_cyclotomic  _ _ 7 (nat.prime.pos prime_7),
  rw nat.prime.proper_divisors prime_7,
  simp only [finset.prod_singleton, cyclotomic_one],
  ring
end

lemma mul_15 : 15 = 3 * 5 := by norm_num

lemma mul_21 : 21 = 3 * 7 := by norm_num

lemma mul_35 : 35 = 5 * 7 := by norm_num

lemma cyclotomic_15 : cyclotomic 15  = 1 - X + X ^ 3 - X ^ 4 + X ^ 5 - X ^ 7 + X ^ 8 :=
begin
  apply @compute_cyclotomic  _ _ 15 _,
  { nth_rewrite 0 mul_15,
    rw [proper_divisors_semiprime prime_3 prime_5 _, finset.prod_insert (not_mem_two _ _),
    finset.prod_insert (not_mem_singleton _), finset.prod_singleton, cyclotomic_one, cyclotomic_3,
    cyclotomic_5],
    repeat { norm_num },
    ring },
  norm_num
end

lemma cyclotomic_21 : cyclotomic 21  =
  1 - X + X ^ 3 - X ^ 4 + X ^ 6 - X ^ 8 + X ^ 9 - X ^ 11 + X ^ 12 :=
begin
  apply @compute_cyclotomic  _ _ 21 _,
  { nth_rewrite 0 mul_21,
    rw [proper_divisors_semiprime prime_3 prime_7 _, finset.prod_insert (not_mem_two _ _),
    finset.prod_insert (not_mem_singleton _), finset.prod_singleton, cyclotomic_one, cyclotomic_3,
    cyclotomic_7],
    repeat { norm_num },
    ring },
  norm_num
end

lemma cyclotomic_35 : cyclotomic 35  =
  1 - X + X ^ 5 - X ^ 6 + X ^ 7 - X ^ 8 + X ^ 10 - X ^ 11 + X ^ 12 - X ^ 13 + X ^ 14 - X ^ 16 +
  X ^ 17 - X ^ 18 + X ^ 19 - X ^ 23 + X ^ 24 :=
begin
  apply @compute_cyclotomic  _ _ 35 _,
  { nth_rewrite 0 mul_35,
    rw [proper_divisors_semiprime prime_5 prime_7 _, finset.prod_insert (not_mem_two _ _),
    finset.prod_insert (not_mem_singleton _), finset.prod_singleton, cyclotomic_one, cyclotomic_5,
    cyclotomic_7],
    repeat { norm_num },
    ring },
  norm_num
end

lemma fact_105 : 105 = 3 * (5 * 7) := by norm_num

lemma card_explicit : ({1, 3, 5, 7, 15, 21, 35} : finset ).card = 7 := rfl

lemma proper_divisors_105 : nat.proper_divisors (105) = {1, 3, 5, 7, 15, 21, 35} :=
begin
  symmetry,
  rw fact_105,
  apply finset.eq_of_subset_of_card_le,
  { rw finset.subset_iff,
    norm_num },
  rw [proper_divisors_three_primes_card prime_3 prime_5 prime_7 _ _ _, card_explicit],
  repeat { norm_num }
end

lemma cyclotomic_105 : cyclotomic 105  =
  1 + X + X ^ 2 - X ^ 5 - X ^ 6 - 2 * X ^ 7 - X ^ 8 - X ^ 9 + X ^ 12 + X ^ 13 + X ^ 14 + X ^ 15
  + X ^ 16 + X ^ 17 - X ^ 20 - X ^ 22 - X ^ 24 - X ^ 26 - X ^ 28 + X ^ 31 + X ^ 32 + X ^ 33 +
  X ^ 34 + X ^ 35 + X ^ 36 - X ^ 39 - X ^ 40 - 2 * X ^ 41 - X ^ 42 - X ^ 43 + X ^ 46 + X ^ 47 +
  X ^ 48 :=
begin
  apply @compute_cyclotomic  _ _ 105 _,
  { rw proper_divisors_105,
    repeat {rw finset.prod_insert _},
    rw [finset.prod_singleton, cyclotomic_one, cyclotomic_3, cyclotomic_5, cyclotomic_7,
    cyclotomic_15, cyclotomic_21, cyclotomic_35],
    ring,
    repeat { simp only [finset.mem_insert, finset.mem_singleton], norm_num } },
  norm_num
end

view this post on Zulip Mario Carneiro (Nov 07 2020 at 17:08):

Here's a way to compute all the numerical stuff by refl:

lemma cyclotomic_15 : cyclotomic 15  = 1 - X + X ^ 3 - X ^ 4 + X ^ 5 - X ^ 7 + X ^ 8 :=
begin
  apply @compute_cyclotomic  _ _ 15 pos_of_15,
  nth_rewrite 0 mul_15,
  change (3 * 5 : ).proper_divisors with quot.mk _ [1, 3, 5], _⟩,
  simp [cyclotomic_one, cyclotomic_3, cyclotomic_5],
  ring
end

view this post on Zulip Mario Carneiro (Nov 07 2020 at 17:13):

In general, it is much harder to prove that {0,1,2,3,4,5}.card = 6 than (finset.range 6).card 6. The reason is that the former involves 5 calls to finset.insert, which has to deduplicate the set, while finset.range 6 boils down to <[0,1,2,3,4,5],stuff>.card = 6 which reduces to [0,1,2,3,4,5].length = 6 which is easy

view this post on Zulip Mario Carneiro (Nov 07 2020 at 17:13):

in particular, you never have to prove the numbers are distinct

view this post on Zulip Mario Carneiro (Nov 07 2020 at 17:14):

because it's encoded in the construction mechanism

view this post on Zulip Riccardo Brasca (Nov 07 2020 at 17:58):

I have to learn about change!

view this post on Zulip Adam Topaz (Nov 07 2020 at 18:36):

The good and/or bad thing about change is that you have to know how things are defined :rofl:

view this post on Zulip Aaron Anderson (Nov 07 2020 at 22:56):

Also, for the record, we have actually had enough Gauss's lemma for cyclotomic polynomials for months...

view this post on Zulip Aaron Anderson (Nov 07 2020 at 22:56):

polynomial.irreducible_of_irreducible_map only needs the polynomial to be monic

view this post on Zulip Riccardo Brasca (Nov 08 2020 at 12:17):

That's a great news! I will soon start working on irreducibility, and then I plan to prove that for all nn there infinitely many primes pp with p1modpp \equiv 1 \bmod{p} (and maybe also p1modpp \equiv -1 \bmod{p}, if I remember correctly the proof is essentially the same).

view this post on Zulip Kevin Buzzard (Nov 08 2020 at 12:39):

I didn't know -1 mod N was possible with elementary methods!

view this post on Zulip Riccardo Brasca (Nov 08 2020 at 12:54):

Ah yes, I had in mind an exercise I did during my master , but indeed it says to prove that there are infinitely many primes pp with p1modnp \equiv 1 \bmod{n}, and infinitely many with p≢1modnp \not\equiv 1 \bmod{n}, no 1-1. :innocent:

view this post on Zulip Kevin Buzzard (Nov 08 2020 at 13:19):

There's a very easy proof that there are infinitely many primes not in a given proper subgroup of (Z/nZ)×(\mathbb{Z}/n\mathbb{Z})^\times (given finitely many primes not in it, mutiply them all together, raise to the power ϕ(n)\phi(n) and then add a small number to get out of the subgroup; this can be made to work).

view this post on Zulip Marc Masdeu (Nov 09 2020 at 10:08):

Ram Murty proved the very nice result that a "Euclidean proof" of the existence of infinitely many primes pamodnp \equiv a \mod n exists if and only if a21modna^2\equiv 1 \mod n. Both directions are really cool and somewhat surprising...

view this post on Zulip Riccardo Brasca (Nov 20 2020 at 09:55):

I have almost finished proving the irreducibility of cyclotomic n ℤ. I have a proof that the minimal polynomial of μ is the same as the minimal polynomial of μ ^ p, where μ is a primitive nth root of unity and p is a prime that does not divide n. This is 90% of the proof of irreducible (cyclotomic n ℤ), but in the proof there is no need to mention cyclotomic n ℤ. It is around 250 lines and. I need an advice: should I put it in ring_theory/roots_of_unity (or in analysis/comples/roots_of_unity since it concerns complex roots of unity, even if technically I don't need the results proved there) or in ring_theory/polynomials/cyclotomic? In the latter case it is maybe reasonable to create a folder ring_theory/polynomials/cyclotomic with two files basic (the current cyclotomic.lean) and irreducible. Thank you !

view this post on Zulip Johan Commelin (Nov 20 2020 at 09:57):

I would do whatever minimizes imports

view this post on Zulip Johan Commelin (Nov 20 2020 at 09:57):

I think it makes sense to avoid an import *.complex.* in ring_theory/roots_of_unity

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 09:58):

Mathematically this looks to me like a result about roots of unity. Does the proof work over an arbitrary field (for which the primitive n'th root exists)? Presumably.

view this post on Zulip Riccardo Brasca (Nov 20 2020 at 10:02):

I don't need any results of analysis/comples/roots_of_unity, I just start taking μ a complex primitive roots, so I suppose existence. Indeed, as Kevin says, I can replace by any characteristic 0 domain R, assuming the existence of a primitive root of unity in R.

view this post on Zulip Riccardo Brasca (Nov 20 2020 at 10:02):

Here are the imports

import ring_theory.polynomial.gauss_lemma
import field_theory.separable
import field_theory.finite.basic

view this post on Zulip Johan Commelin (Nov 20 2020 at 10:03):

If you work over arbitrary R, why do you need the last import?

view this post on Zulip Johan Commelin (Nov 20 2020 at 10:04):

Anyway, with these imports, I guess it makes most sense to add this stuff to ring_theory/roots_of_unity

view this post on Zulip Riccardo Brasca (Nov 20 2020 at 10:05):

The minimal polynomial is still over . The proof works by reduction modulo p (where P(xp)=P(x)pP(x^p) = P(x)^p for a polynomial PP).

view this post on Zulip Johan Commelin (Nov 20 2020 at 10:11):

Ok, sure

view this post on Zulip Riccardo Brasca (Nov 28 2020 at 16:47):

Can someone suggest names for the following lemmas?

/-- If `(a : ℕ)` is a root of `cyclotomic n (zmod p)`, where `p` is a prime, then `a` and `p` are
coprime. -/
lemma test1 {n : } (hpos : 0 < n) {p : } [hprime : fact p.prime] {a : }
  (hroot : is_root (cyclotomic n (zmod p)) (nat.cast_ring_hom (zmod p) a)) :
  a.coprime p

/-- If `(a : ℕ)` is a root of `cyclotomic n (zmod p)`, where `p` is a prime that does not divide
`n`, then the multiplicative order of `a` modulo `p` is exactly `n`. -/
lemma test2 {n : } (hpos : 0 < n) {p : } [hprime : fact p.prime] {a : } (hn : ¬ p  n) (hroot : is_root (cyclotomic n (zmod p)) (nat.cast_ring_hom (zmod p) a)) :
  order_of (zmod.unit_of_coprime a (test1 hpos hroot)) = n

I am thinking about something like coprime_of_root_cyclotomic for the first one, and I really don't know for the second (the first one is in the polynomial namespace).

Also, test2 is the main arithmetic step in the proof that there infinitely many primes congruent to 1 modulo n. I am wondering if it will be reasonable to put it in a separate file, with the proof of the theorem.


Last updated: May 12 2021 at 08:14 UTC