Mathlib v3 is deprecated. Go to Mathlib v4

Theorem to_subalgebra_to_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 to_subalgebra_to_intermediate_field View on Github →