Mathlib v3 is deprecated. Go to Mathlib v4

Theorem lift.subfield_with_hom.maximal_subfield_with_hom_eq_top

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_eq_topView on Github →