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) …

Added to_intermediate_field'_to_subalgebra View on Github →