Mathlib v3 is deprecated. Go to Mathlib v4

Theorem lift.subfield_with_hom.exists_maximal_subfield_with_hom

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.exists_maximal_subfield_with_homView on Github →