Mathlib v3 is deprecated. Go to Mathlib v4

Def subalgebra_equiv_intermediate_field

Modification history

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 subalgebra_equiv_intermediate_fieldView on Github →