## Stream: maths

### Topic: Definition of polynomial.splits

#### Yury G. Kudryashov (Oct 20 2020 at 04:02):

Why docs#polynomial.splits uses an auxiliary ring_hom?

#### Yury G. Kudryashov (Oct 20 2020 at 04:02):

I mean, why not define

def splits (f : polynomial α) : Prop :=
f = 0 ∨ ∀ {g : polynomial α}, irreducible g → g ∣ f → degree g = 1


then use splits (map i f) if needed?

@Kenny Lau :up:

#### Mario Carneiro (Oct 20 2020 at 04:30):

From a cursory look at the original definition, it looks not equivalent, because it has a disjunct f = 0 instead of map i f = 0

#### Mario Carneiro (Oct 20 2020 at 04:30):

What does the mathematics have to say about the cases where there is a difference?

#### Yury G. Kudryashov (Oct 20 2020 at 04:33):

docs#polynomial.splits_map_iff

#### Yury G. Kudryashov (Oct 20 2020 at 04:34):

docs#polynomial.map_eq_zero

#### Johan Commelin (Oct 20 2020 at 04:35):

I think mathematics doesn't really care about whether 0 splits or not. That's an implementation detail, and we can choose whatever we find most convenient.

#### Mario Carneiro (Oct 20 2020 at 04:35):

wait, is the codomain a field here?

#### Mario Carneiro (Oct 20 2020 at 04:35):

oh everything is a field

#### Mario Carneiro (Oct 20 2020 at 04:38):

ah, docs#polynomial.splits_id_iff_splits is even more explicit that this can be a unary predicate

#### Mario Carneiro (Oct 20 2020 at 04:42):

I guess the other question is whether the theorems in there follow easily from theorems about splits id and map

#### Kenny Lau (Oct 20 2020 at 07:01):

I believe @Chris Hughes wrote it

Last updated: May 11 2021 at 15:12 UTC