mathlib

e57fc3d6 - feat(field_theory/splitting_field): splitting field unique (#3654)

feat(field_theory/splitting_field): splitting field unique (#3654) Main theorem: ```lean polynomial.is_splitting_field.alg_equiv {α} (β) [field α] [field β] [algebra α β] (f : polynomial α) [is_splitting_field α β f] : β ≃ₐ[α] splitting_field f ```` Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>