intermediate_field.adjoin_splits

Stream: Is there code for X?

[Adam Topaz]

Do we have the following lemma or some variant that makes it easy to prove?

import field_theory.adjoin

universe u
variables (F : Type u) [field F] (L : Type*) [field L] [algebra F L]

lemma intermediate_field.adjoin_splits (f : polynomial F) (hf : f.splits (algebra_map F L)) :
  f.splits (algebra_map F (intermediate_field.adjoin F {x : L | polynomial.aeval x f = 0})) :=
sorry

(sorry, fixed the import, that should be a mwe now)

[Thomas Browning]

My guess is that we don't have that. Side comment: you might be able to use docs#polynomial.root_set