Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-16 10:37 b7593841

View on Github →

feat(field_theory/algebraic_closure): map from algebraic extensions into the algebraic closure (#9110)

Estimated changes

Modified src/field_theory/algebraic_closure.lean

added theorem is_alg_closed.exists_aeval_eq_zero

added theorem is_alg_closed.exists_eval₂_eq_zero

modified theorem is_alg_closed.exists_root

added def is_alg_closed.lift

added theorem lift.subfield_with_hom.compat

added theorem lift.subfield_with_hom.exists_maximal_subfield_with_hom

added theorem lift.subfield_with_hom.le_def

added def lift.subfield_with_hom.maximal_subfield_with_hom

added theorem lift.subfield_with_hom.maximal_subfield_with_hom_chain_bounded

added theorem lift.subfield_with_hom.maximal_subfield_with_hom_eq_top

added theorem lift.subfield_with_hom.maximal_subfield_with_hom_is_maximal

added structure lift.subfield_with_hom

Modified src/ring_theory/algebraic.lean