Definition of `polynomial.splits`

Stream: maths

[Yury G. Kudryashov]

Why docs#polynomial.splits uses an auxiliary ring_hom?

[Yury G. Kudryashov]

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?

[Johan Commelin]

@Kenny Lau :up:

[Mario Carneiro]

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]

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

[Yury G. Kudryashov]

docs#polynomial.splits_map_iff

[Yury G. Kudryashov]

docs#polynomial.map_eq_zero

[Johan Commelin]

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]

wait, is the codomain a field here?

[Mario Carneiro]

oh everything is a field

[Mario Carneiro]

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

[Mario Carneiro]

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

[Yury G. Kudryashov]

#4708 #4709

[Kenny Lau]

I believe @Chris Hughes wrote it