Murty's irreducibility criterion

Stream: mathlib4

[Daniel Weber]

I'm proving theorem 1 from https://mast.queensu.ca/%7Emurty/monthly.pdf, and I want to generalize it

[Johan Commelin]

I'm curious what ingredients are needed for this result. Using the complex numbers feels like it is over-powered

[Riccardo Brasca]

I see. Not sure the norm defined in number theory is relevant here.

[Daniel Weber]

Johan Commelin said:

I'm curious what ingredients are needed for this result. Using the complex numbers feels like it is over-powered

It seems quite hard to lower-bound the values of the factors without looking at complex roots

[Notification Bot]

4 messages were moved here from #Is there code for X? > Algebras where elements have integer norm by Johan Commelin.

[Johan Commelin]

@Daniel Weber By the way, what is your definition of Murty's H?

[Daniel Weber]

noncomputable def H (p : K[X]) (hp : p.natDegree ≠ 0) : ℝ :=
  sup' (range p.natDegree) (by simpa) (fun x ↦ ‖(p.coeff x : T) / p.leadingCoeff‖)

[Johan Commelin]

I wonder whether it pays off to get rid of hp (using some if .. then .. else)

[Daniel Weber]

I think that's what I'll do in the version I PR, yeah

[Eric Wieser]

I commented this on the PR already; but using nnnorm and sup also avoids the need for hp

[Antoine Chambert-Loir]

@Johan Commelin this is a kind of “product formula” proof which requires all places of Q, so I don't see how real or complex numbers can be avoided.

[Johan Commelin]

I guess you are right. But where are the p-adic places coming in? (I admit I only thought about this for 10sec)

[Antoine Chambert-Loir]

By the overall use of Int. (Product formula = a non zero integer is at least 1.)

[Johan Commelin]

Aha! Thanks