minpoly fallout

Stream: Berkeley Lean Seminar

[Johan Commelin]

In the minpoly refactor I turned some assumptions involving existentials into things like

(hK : ∀ s ∈ S, is_integral F (s : E) ∧ (minpoly F s).splits (algebra_map F K))

(I think in 3 or 4 places in mathlib.)

To keep the refactor small, I didn't do anything else.
But I guess we can now go a step further:

1. Either we can split the and into two assumptions. Or
2. I guess we can replace the first part by a (typeclass?) assumption that the extension E/F is integral/algebraic.

My preference would be for (2). What do you think?

[Thomas Browning]

My preference would be for (1). I'd rather leave open the possibility of working with intermediatte_field ℚ ℂ, for instance.

[Patrick Lutz]

I agree with Thomas

[Johan Commelin]

Yes, I agree (1) is better.