Commit 2022-07-29 14:31 7afd66ab

View on Github →

feat(field_theory/intermediate_field): Produce an intermediate field from a subalgebra satisfying is_field. (#15659) This construction came up when proving that if p splits in L/K, then p.is_splitting_field K (adjoin K (p.root_set L)).

Estimated changes

Modified src/field_theory/intermediate_field.lean

added def subalgebra.to_intermediate_field'

added theorem to_intermediate_field'_to_subalgebra

modified theorem to_intermediate_field_to_subalgebra

added theorem to_subalgebra_to_intermediate_field'