# Zulip Chat Archive

## Stream: new members

### Topic: Strange behavior of `mul_eq_zero`

#### Riccardo Brasca (Nov 14 2020 at 23:58):

I am trying to prove that the minimal polynomial of an element `x`

is irreducible, without the assumption that the base ring is a field, but only an integral domain. It's rather annoying (if someone see a quick way to do it all suggestions are welcome...). At some point I need to use that if the minimal polynomial is the product `a * b`

then `x`

is a root of `a`

or of `b`

: this should be easy, and I wanted to use `mul_eq_zero`

as in the following code

```
import field_theory.minimal_polynomial
universes u v
open_locale classical
variables {α : Type u} {β : Type v}
namespace minimal_polynomial
variables [integral_domain α] [ring β] [algebra α β] {x : β} (hx : is_integral α x)
lemma test [integral_domain β] : _root_.irreducible (minimal_polynomial hx) :=
begin
have not_unit : ¬ is_unit (minimal_polynomial hx),
{ sorry },
cases irreducible_or_factor (minimal_polynomial hx) not_unit with hirr hred,
{ exact hirr },
obtain ⟨a, hred⟩ := hred,
obtain ⟨b, hred⟩ := hred,
have hzero : polynomial.aeval x a = 0 ∨ polynomial.aeval x b = 0,
{ apply mul_eq_zero.1,
{ sorry },
have h₁ := integral_domain.to_domain β,
have h₂ := @domain.to_no_zero_divisors β h₁,
--exact h₂ does not work
sorry
},
sorry
end
end minimal_polynomial
```

Ignore the `sorry`

, my problem is where the comment is. As you can see `mul_eq_zero`

asks to prove `no_zero_divisors β`

, that is already strange since there is `[integral_domain β]`

in the assumptions, but even if I try to do it it complains with some errors that I do not understand. Indeed `h₂`

seems to be exactly what it wants, but `exact h₂`

doesn't work.

What's going on? Thank you!

#### Alex J. Best (Nov 15 2020 at 00:06):

I get an error at not_is_unit.

#### Alex J. Best (Nov 15 2020 at 00:06):

Could it be becasue you have ring beta and integral domain beta?

#### Aaron Anderson (Nov 15 2020 at 00:10):

Alex J. Best said:

Could it be becasue you have ring beta and integral domain beta?

I tried replacing the original `[ring beta]`

with `[integral_domain beta]`

and deleting the second `[integral_domain beta]`

, it fixed this.

#### Aaron Anderson (Nov 15 2020 at 00:11):

It might not fix `not_is_unit`

, because `not_is_unit`

currently requires a field, but @Riccardo Brasca probably has modified `not_is_unit`

locally.

#### Riccardo Brasca (Nov 15 2020 at 00:12):

@Alex J. Best Ah yes sorry! That's because I have modified `not_is_unit`

in `minimal_polynomial`

, now it should work.

#### Riccardo Brasca (Nov 15 2020 at 00:14):

Ah ok, I still do not understand clearly what to do to add assumptions like this...

#### Alex J. Best (Nov 15 2020 at 00:15):

integral domain includes a ring structure, so when you have `ring X`

and `integral_domain X`

you have introduced two (independent) ring structures on the same type which confuses lean.

#### Riccardo Brasca (Nov 15 2020 at 00:17):

But what is the general strategy if I am working with `variable [ring R]`

defined somewhere and in a lemma I need `[integral_domain R]`

?

#### Aaron Anderson (Nov 15 2020 at 00:17):

The best way to deal with this is to use the `section`

command to have a section of your file where you start by defining `variables [ring beta]`

and whatever other instances you want, for your general ring theorems, and then a new section starting with `variables [integral_domain beta]`

for your integral domain theorems

#### Riccardo Brasca (Nov 15 2020 at 00:17):

@Aaron Anderson You almost answered my question *before* I asked it!

#### Aaron Anderson (Nov 15 2020 at 00:18):

Another potential strategy is to use `[ring R]`

and then later `[is_integral_domain R]`

, but you won't always have that flexibility, and I'd still recommend going with the multiple sections.

#### Riccardo Brasca (Nov 15 2020 at 00:55):

I've put the (ugly) proof in quote #5006.

#### Aaron Anderson (Nov 15 2020 at 04:41):

I could help golf this down, but the way this currently works for fields is a sequence of lemmas.

#### Aaron Anderson (Nov 15 2020 at 04:41):

Do we know if some of them might work for a wider class of domains?

#### Aaron Anderson (Nov 15 2020 at 04:42):

Well, I guess we know that the second-to-last lemma, `minimal_polynomial.prime`

, definitely works for gcd or unique factorization domains, because that's equivalent to irreducible there

#### Aaron Anderson (Nov 15 2020 at 06:33):

I think that the whole slew of results for fields should also hold for integrally closed domains - I think I read that minimal polynomials over integrally closed domains equal the minimal polynomial over the fraction field, which is really the key result here

#### Riccardo Brasca (Nov 15 2020 at 10:17):

I think that at the end everything boils down to en even stronger version of Gauss's lemma than the one I asked yesterday: If $P \in R[X]$ is primitive and $P = Q_1 \cdot Q_2$ is a non trivial factorization in $K[X]$ then essentially $Q_1$ and $Q_2$ are already in $R[X]$ (I mean, up to multiplication and division by a scalar). For PID I have a simple proof, I do not know a proof for integrally closed domain (if it is true...) and here http://www-users.math.umn.edu/~garrett/m/algebra/notes/12.pdf there is a proof for UFD that seems to be a proof for GCD domains. (Essentially he consider divisibility in $K$ considering only multiplication by elements of $R$ and he proves Gauss's lemma in this context.)

Last updated: Dec 20 2023 at 11:08 UTC