Mathlib v3 is deprecated. Go to Mathlib v4

Theorem to_subalgebra_to_intermediate_field'

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_subalgebra_to_intermediate_field'View on Github →