Zulip Chat Archive

Stream: maths

Topic: Cyclotomic polynomials

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 :)

Johan Commelin (Sep 17 2020 at 15:45):

@Kenny Lau @Kevin Buzzard :up:

Kenny Lau (Sep 17 2020 at 15:52):

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

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 $\Psi_d$ :
1) minimal polynomial of $\exp(2\pi i/n)$
2) $\prod_{{\zeta} \in \mu^\ast} (X - \zeta)$ , where $\mu^\ast$ is the set of primitive root of unity.

Kenny Lau (Sep 17 2020 at 15:57):

I prefer 1

Kenny Lau (Sep 17 2020 at 15:57):

because it's in Z[x] automatically

Kenny Lau (Sep 17 2020 at 15:58):

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

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.

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...)

Adam Topaz (Sep 17 2020 at 15:59):

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

Adam Topaz (Sep 17 2020 at 16:01):

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

Riccardo Brasca (Sep 17 2020 at 16:01):

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

Riccardo Brasca (Sep 17 2020 at 16:01):

@Adam Topaz I will check it.

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

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.

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.

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

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).

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.

Riccardo Brasca (Sep 17 2020 at 16:26):

By the way, I am stuck with the very stupid fact that $\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

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

Kenny Lau (Sep 17 2020 at 16:30):

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

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

Johan Commelin (Sep 17 2020 at 16:32):

@Riccardo Brasca :up:

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

Johan Commelin (Sep 17 2020 at 16:34):

You were pretty close already

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,

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...)

Johan Commelin (Sep 17 2020 at 16:37):

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

Riccardo Brasca (Sep 17 2020 at 16:37):

Ah, there is field_simp!

Johan Commelin (Sep 17 2020 at 16:37):

Then field_simp can use that fact to cancel the division.

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 (-;

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.

Riccardo Brasca (Sep 17 2020 at 16:41):

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

Heather Macbeth (Sep 17 2020 at 16:43):

That one does exist! docs#complex.exp_pi_mul_I

Heather Macbeth (Sep 17 2020 at 16:44):

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

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

Riccardo Brasca (Sep 17 2020 at 17:20):

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

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

Kenny Lau (Sep 17 2020 at 17:21):

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

Johan Commelin (Sep 17 2020 at 17:21):

Riccardo Brasca said:

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

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

Johan Commelin (Sep 17 2020 at 17:22):

Right, and n \ne 0

Riccardo Brasca (Sep 17 2020 at 17:22):

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

Johan Commelin (Sep 17 2020 at 17:23):

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

Johan Commelin (Sep 17 2020 at 17:24):

Note that there is a lemma X_pow_sub_C_ne_zero

Johan Commelin (Sep 17 2020 at 17:24):

Together with C_1, that will make the proof easy.

Riccardo Brasca (Sep 17 2020 at 17:25):

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

Riccardo Brasca (Sep 17 2020 at 17:35):

I finished the definition of $\Psi_d$ as minimal polynomial over $\mathbf{Q}$ of $\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 $\Psi_d \in \mathbf{Q}[X]$ is irreducible. Tomorrow I will try to prove that it is actually in $\mathbf{Z}[X]$ and see if I can prove the formula for $X^d - 1$ . Thank you for all your comments!!

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

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

Johan Commelin (Sep 17 2020 at 17:45):

Still has one sorry left.

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?

Kevin Buzzard (Sep 17 2020 at 17:58):

What is the type of roots f?

Adam Topaz (Sep 17 2020 at 17:58):

multiset right?

Johan Commelin (Sep 17 2020 at 17:59):

eq_prod_roots_of_splits

Adam Topaz (Sep 17 2020 at 17:59):

Otherwise why would anyone ever use multiset.map?

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 $X^n - 1 = \prod_{d | n} \Psi_d$ in a week or so.

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

Adam Topaz (Sep 17 2020 at 18:08):

roots 0 seems to be defined as $\varnothing$ .

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

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 $\mathbf{Z}$ assuming the element is integral?

Cool. I didn't know that existed.

Riccardo Brasca (Sep 17 2020 at 18:11):

Yes, integral coefficients is not a problem.

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 (\Phi_n) = \phi(n)$ holds with https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Arithmetic.20Functions/near/209952965

Adam Topaz (Sep 17 2020 at 18:12):

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

Adam Topaz (Sep 17 2020 at 18:18):

I think $\Phi_0 = 1$ is a sensible choice.

Johan Commelin (Sep 17 2020 at 19:31):

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

Adam Topaz (Sep 17 2020 at 19:31):

I was thinking of the fact that the limit of $n$ in $\widehat{\mathbf{Z}}$ is $0$ with respect to divisibility.

Johan Commelin (Sep 17 2020 at 19:36):

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

Johan Commelin (Sep 17 2020 at 19:38):

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

Adam Topaz (Sep 17 2020 at 19:38):

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

Johan Commelin (Sep 17 2020 at 19:38):

Nope...

Adam Topaz (Sep 17 2020 at 19:39):

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

Adam Topaz (Sep 17 2020 at 19:40):

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

$\widehat{\mathbf{Z}} \cong \prod_p \mathbf{Z}_p.$

Adam Topaz (Sep 17 2020 at 19:41):

Or maybe it should be extended to supernatural numbers.

Joseph Myers (Sep 17 2020 at 19:48):

Kenny Lau said:

Riccardo Brasca the main lemma is to show that $\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.

Johan Commelin (Sep 17 2020 at 19:49):

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

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

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 > 0$ .

Riccardo Brasca (Sep 17 2020 at 23:43):

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

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

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?

Kenny Lau (Sep 18 2020 at 07:13):

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

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 $\mathbf{Z}$ (to prove that $\Phi_d$ is irreducible over $\mathbf{Q}$ ).

Johan Commelin (Sep 18 2020 at 15:20):

Nope, I don't think so

Aaron Anderson (Nov 01 2020 at 02:36):

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

Aaron Anderson (Nov 01 2020 at 02:37):

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

Thomas Browning (Nov 01 2020 at 02:38):

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

Thomas Browning (Nov 01 2020 at 02:39):

Or maybe I have your question the wrong way around

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.

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 :)

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.

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.

Kevin Buzzard (Nov 01 2020 at 19:19):

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

Riccardo Brasca (Nov 01 2020 at 19:36):

I will try to do it.

Johan Commelin (Nov 06 2020 at 16:04):

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

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.

Kevin Buzzard (Nov 06 2020 at 17:48):

The famous counterexample!

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 :-)

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.

Filippo A. E. Nuccio (Nov 06 2020 at 19:18):

Good luck :wink:

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

Johan Commelin (Nov 06 2020 at 19:25):

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

Johan Commelin (Nov 06 2020 at 19:25):

But we don't have Mobius yet...

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.

Johan Commelin (Nov 06 2020 at 19:26):

Maybe a specific "plugin" could do it?

Mario Carneiro (Nov 06 2020 at 19:26):

a plugin could do it

Mario Carneiro (Nov 06 2020 at 19:26):

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

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

Mario Carneiro (Nov 06 2020 at 19:29):

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

Mario Carneiro (Nov 06 2020 at 19:29):

is this proven?

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

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

Kevin Buzzard (Nov 06 2020 at 19:34):

Mario Carneiro said:

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

Another alternative is $\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.

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

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

Mario Carneiro (Nov 06 2020 at 19:36):

wikipedia seems to make an exception to the table for 105

Kevin Buzzard (Nov 06 2020 at 20:07):

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

Riccardo Brasca (Nov 06 2020 at 20:07):

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

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 :)

Riccardo Brasca (Nov 06 2020 at 20:09):

Ah, I see that you predicted my strategy :)

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?

Riccardo Brasca (Nov 06 2020 at 20:20):

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

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)?

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

Mario Carneiro (Nov 06 2020 at 20:32):

You should use nat.factors, which is a list

Mario Carneiro (Nov 06 2020 at 20:32):

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

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:

Mario Carneiro (Nov 07 2020 at 02:21):

what's the proof?

Johan Commelin (Nov 07 2020 at 06:58):

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

Kevin Buzzard (Nov 07 2020 at 07:21):

Well done! Getting lean to calculate is hard work!

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.

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?

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

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.

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.

Reid Barton (Nov 07 2020 at 12:59):

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

Reid Barton (Nov 07 2020 at 12:59):

Is your comment about nat.divisors related to this?

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.

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.

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.

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

Reid Barton (Nov 07 2020 at 13:12):

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

Reid Barton (Nov 07 2020 at 13:12):

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

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

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.

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)

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

Riccardo Brasca (Nov 07 2020 at 13:27):

Aahh, it's a matter of decidable_eq!

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

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.

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.

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.

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 $\{\sum_{n\geq1}n^{-2},\pi^2/6\}$ ; one has to prove a theorem first to compute the size of this set.

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!

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

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

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

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

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

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.

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

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

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

Mario Carneiro (Nov 07 2020 at 17:13):

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

Mario Carneiro (Nov 07 2020 at 17:14):

because it's encoded in the construction mechanism

Riccardo Brasca (Nov 07 2020 at 17:58):

I have to learn about change!

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:

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

Aaron Anderson (Nov 07 2020 at 22:56):

polynomial.irreducible_of_irreducible_map only needs the polynomial to be monic

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 $n$ there infinitely many primes $p$ with $p \equiv 1 \bmod{p}$ (and maybe also $p \equiv -1 \bmod{p}$ , if I remember correctly the proof is essentially the same).

Kevin Buzzard (Nov 08 2020 at 12:39):

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

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 $p$ with $p \equiv 1 \bmod{n}$ , and infinitely many with $p \not\equiv 1 \bmod{n}$ , no $-1$ . :innocent:

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 $(\mathbb{Z}/n\mathbb{Z})^\times$ (given finitely many primes not in it, mutiply them all together, raise to the power $\phi(n)$ and then add a small number to get out of the subgroup; this can be made to work).

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 $p \equiv a \mod n$ exists if and only if $a^2\equiv 1 \mod n$ . Both directions are really cool and somewhat surprising...

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 !

Johan Commelin (Nov 20 2020 at 09:57):

I would do whatever minimizes imports

Johan Commelin (Nov 20 2020 at 09:57):

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

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.

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.

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

Johan Commelin (Nov 20 2020 at 10:03):

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

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

Riccardo Brasca (Nov 20 2020 at 10:05):

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

Johan Commelin (Nov 20 2020 at 10:11):

Ok, sure

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.

Riccardo Brasca (May 18 2021 at 12:29):

Is it reasonable to put the counterexample above (a cyclotomic polynomial with a coefficients different from 0, 1 and -1) in the counterexamples folder?

Damiano Testa (May 18 2021 at 12:43):

I am in favour of this!

Riccardo Brasca (May 18 2021 at 12:46):

OMG

lemma proper_divisors_105 : nat.proper_divisors (105) = {1, 3, 5, 7, 15, 21, 35} := rfl

works!! I spent hours to prove it...

Kevin Buzzard (May 18 2021 at 13:01):

I suspect there is some Mario magic going on behind the scenes here...

Eric Wieser (May 18 2021 at 13:11):

I think the key is that it's a finset (and you got the order right so that there is no need to use quotient.sound)

Eric Wieser (May 18 2021 at 13:11):

src#nat.proper_divisors is very simple

Riccardo Brasca (May 18 2021 at 13:30):

#7648 At the end it is quite easy

Last updated: Dec 20 2023 at 11:08 UTC