mathlib

b874abc7 - feat(field_theory): state primitive element theorem using `power_basis` (#8073)

feat(field_theory): state primitive element theorem using `power_basis` (#8073) This PR adds an alternative formulation to the primitive element theorem: the original formulation was `∃ α : E, F⟮α⟯ = (⊤ : intermediate_field F E)`, which means a lot of pushing things across the equality/equiv from `F⟮α⟯` to `E` itself. I claim that working with a field `E` that has a power basis over `F` is nicer since you don't need to do a lot of transporting.