Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-06 16:42 e57fc3d6

View on Github →

feat(field_theory/splitting_field): splitting field unique (#3654) Main theorem:

polynomial.is_splitting_field.alg_equiv {α} (β) [field α] [field β] [algebra α β]
  (f : polynomial α) [is_splitting_field α β f] : β ≃ₐ[α] splitting_field f

Estimated changes