Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-11 10:10 b537cc08

View on Github →

feat(algebra/splitting_field): Restrict to splitting field (#5562) Restrict an alg_hom or alg_equiv to an is_splitting_field.

Estimated changes

Modified src/field_theory/splitting_field.lean

added def alg_equiv.restict_is_splitting_field_hom

added def alg_equiv.restrict_is_splitting_field

added theorem alg_equiv.restrict_is_splitting_field_commutes

added theorem alg_equiv.restrict_is_splitting_field_trans

added def alg_hom.restrict_is_splitting_field

added def alg_hom.restrict_is_splitting_field_aux

added theorem alg_hom.restrict_is_splitting_field_commutes

added theorem alg_hom.restrict_is_splitting_field_comp

added theorem is_splitting_field.range_to_alg_hom