Mathlib v3 is deprecated. Go to Mathlib v4

Theorem lift.subfield_with_hom.maximal_subfield_with_hom_is_maximal

Modification history

2021-09-16 10:37
src/field_theory/algebraic_closure.lean
feat(field_theory/algebraic_closure): map from algebraic extensions into the algebraic closure (#9110)
Added lift.subfield_with_hom.maximal_subfield_with_hom_is_maximalView on Github →