Mathlib v3 is deprecated. Go to Mathlib v4

Theorem to_intermediate_field_to_subalgebra

Modification history

2022-07-29 14:31
src/field_theory/intermediate_field.lean
feat(field_theory/intermediate_field): Produce an intermediate field from a subalgebra satisfying `is_field`. (#15659) …
Modified to_intermediate_field_to_subalgebraView on Github →
2020-11-04 16:04
src/field_theory/intermediate_field.lean
feat(ring_theory/algebraic): if `L / K` is algebraic, then the subalgebras are fields (#4903)
Added to_intermediate_field_to_subalgebraView on Github →