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

modified theorem ring_equiv.ext
added theorem ring_equiv.symm_trans
added theorem ring_equiv.trans_symm
added theorem multiset.to_finset_map
added theorem list.prod_ne_zero
added theorem multiset.prod_ne_zero
added theorem polynomial.map_prod
added theorem polynomial.map_ne_zero
added theorem polynomial.roots_C
added theorem polynomial.roots_one
added theorem polynomial.roots_zero
added theorem lift_of_splits
added theorem polynomial.roots_map
added theorem dim_eq_zero
added theorem findim_eq_zero
added theorem findim_top
added theorem alg_hom.injective_iff
added theorem subalgebra.mem_res
added def subalgebra.res
added theorem subalgebra.res_inj
added theorem subalgebra.res_top