# Zulip Chat Archive

## Stream: new members

### Topic: Confusion about ≤ in UFD

#### Riccardo Brasca (Nov 18 2020 at 18:44):

Hi, I want to prove that if a separable polynomial $P$ divides a power $Q^n$ then it divides $Q$. I know that the factors of $P$ are simple, by `polynomial.is_unit_of_self_mul_dvd_separable`

or a similar result, but how can I use it? I thought I would have found something like "if the multiplicity of any prime factor in $P$ is less or equal than the multiplicity in $Q$, then $P$ divides $Q$" in `ring_theory.unique_factorization_domain`

. Is what `associates.prod_mono`

actually says? I am not able to find the definition of `≤`

in this case.

#### Kevin Buzzard (Nov 18 2020 at 18:48):

Seems to me that a term of type `factor_set R`

is either a multiset (a.k.a. finite set with multiplicities allowed) of irreducible-elements-of-R-modulo-equivalence, where the equivalence is "differ by a unit", or a "top" element which is presumably used to represent 0.

#### Kevin Buzzard (Nov 18 2020 at 18:50):

`prod`

is a function which takes one of these multisets (so irreducibles, defined up to units) and multiplies them all together to get an element of the UFD, defined up to units. I guess `<=`

will be defined as "divides", which makes sense in this context. So `prod_mono`

says something like "if you have two multisets of factors, one contained in the other, then the product of the smaller set divides the product of the larger set"

#### Riccardo Brasca (Nov 18 2020 at 18:52):

Yes, it is what I think too, but how can I apply this in practice? I mean, transform my `∣`

in `≤`

with some `rw`

.

#### Kevin Buzzard (Nov 18 2020 at 18:55):

I've not ever used this new UFD stuff and don't know my way around the library at all, but I do know that if you knock up a MWE then you're more likely to get a good answer.

#### Kevin Buzzard (Nov 18 2020 at 18:56):

Looking at where `is_unit_of_self_mul_dvd_separable`

is used, I have run into `multiplicity_le_one_of_seperable`

#### Kevin Buzzard (Nov 18 2020 at 18:57):

which is not how you spell `separable`

but it still might help

#### Kevin Buzzard (Nov 18 2020 at 19:00):

Isn't there some general theory of `squarefree`

stuff somewhere? Did I see this in a recent PR? For me, the natural proof would go separable -> squarefree (using this `seperable`

thing) and P squarefree -> P|Q^n->P|Q

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

` src/algebra/squarefree.lean`

was merged 4 days ago

#### Riccardo Brasca (Nov 18 2020 at 19:02):

What I want to prove is

```
import field_theory.separable
variables (F : Type*) [field F] (P : polynomial F) (Q : polynomial F)
open polynomial
lemma divides (hsep : separable P) (hzero : Q ≠ 0) (n : ℕ) (hdiv: P ∣ Q ^ n) : P ∣ Q :=
begin
sorry
end
```

I'll have a look at ``squarefree`

, thank you!

#### Kevin Buzzard (Nov 18 2020 at 19:05):

`is_unit_of_self_mul_dvd_separable`

can be used to prove separable polynomials are `squarefree`

and then it looks like you'll have to get your hands dirty. I suspect that `r`

is squarefree if and only if for all q, r|q^n -> r|q (at least when one has uniqueness of factorization) but this doesn't seem to be in the PR.

#### Kevin Buzzard (Nov 18 2020 at 19:07):

I'm currently working on another branch which doesn't have squarefree so I'm not much help to you :-( You have this `nodup`

thing, so anyone who knows their way around multisets should be able to add it. You'll need that if n>=1 then the finset of factors of q^n and q are the same, and so you'll have an inclusion of finsets, and using nodup you'll be able to get an inclusion of multisets.

#### Riccardo Brasca (Nov 18 2020 at 19:13):

I see that

```
lemma test {α : Type*} [comm_cancel_monoid_with_zero α] {a b : associates.factor_set α} (h : a ≤ b) :
a.prod ∣ b.prod :=
begin
exact associates.prod_mono h,
end
```

works, so lean "knows" that `≤`

means `∣`

. I think I can figure out the rest of the proof.

#### Aaron Anderson (Nov 18 2020 at 20:55):

#### Kevin Buzzard (Nov 18 2020 at 21:22):

I love this place

#### Aaron Anderson (Nov 18 2020 at 21:29):

(Just proven for `squarefree`

, not `separable`

)

#### Riccardo Brasca (Nov 18 2020 at 21:40):

I'm taking care of it, I will make a PR tomorrow.

#### Riccardo Brasca (Nov 18 2020 at 21:58):

#5039 It was really quick :)

#### Kevin Buzzard (Nov 18 2020 at 22:06):

This is the advantage of making all these little steps.

I was reading something by Deligne, describing Grothendieck's work. Deligne said that he would write arguments and everything would be short and simple and easy, and nothing seemed to be happening, and then all of a sudden out of nowhere you had proved something. This is also the mathlib approach. Introduce the concepts which have been proven to be useful and then make the API relating them and one can really make progress in a very elegant way.

Last updated: May 13 2021 at 18:26 UTC