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

#### 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: May 15 2021 at 22:14 UTC