Commit 2022-08-08 21:44 0a34b827

View on Github →

feat(field_theory/splitting_field): Add image_root_set (#15743) This PR adds a short lemma image_root_set and uses it to prove that is_splitting_field is preserved by algebra isomorphisms.

Estimated changes

Modified src/field_theory/splitting_field.lean

added theorem polynomial.adjoin_root_set_eq_range

added theorem polynomial.image_root_set

added theorem polynomial.is_splitting_field.of_alg_equiv