mathlib

452984bb - feat(field_theory/intermediate_field): `minpoly K x = minpoly K (x : L)` (#15946)

feat(field_theory/intermediate_field): `minpoly K x = minpoly K (x : L)` (#15946) This PR adds a lemma stating that `minpoly K x = minpoly K (x : L)` for `x : S` and `S : intermediate_field K L`.