Commit 2023-06-09 23:11 ef9a563b

View on Github →

feat: port FieldTheory.IsAlgClosed.Basic (#4888)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/IsAlgClosed/Basic.lean

added theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly

added theorem IsAlgClosed.algebraMap_surjective_of_isAlgebraic

added theorem IsAlgClosed.algebraMap_surjective_of_isIntegral

added theorem IsAlgClosed.algebra_map_surjective_of_is_integral'

added theorem IsAlgClosed.degree_eq_one_of_irreducible

added theorem IsAlgClosed.exists_aeval_eq_zero

added theorem IsAlgClosed.exists_aeval_eq_zero_of_injective

added theorem IsAlgClosed.exists_eq_mul_self

added theorem IsAlgClosed.exists_eval₂_eq_zero

added theorem IsAlgClosed.exists_eval₂_eq_zero_of_injective

added theorem IsAlgClosed.exists_pow_nat_eq

added theorem IsAlgClosed.exists_root

added theorem IsAlgClosed.of_exists_root

added theorem IsAlgClosed.roots_eq_zero_iff

added theorem IsAlgClosed.splits_codomain

added theorem IsAlgClosed.splits_domain

added theorem IsAlgClosure.equivOfEquiv_algebraMap

added theorem IsAlgClosure.equivOfEquiv_comp_algebraMap

added theorem IsAlgClosure.equivOfEquiv_symm_algebraMap

added theorem IsAlgClosure.equivOfEquiv_symm_comp_algebraMap

added theorem IsAlgClosure.ofAlgebraic

added theorem isAlgClosure_iff

added theorem lift.SubfieldWithHom.compat

added theorem lift.SubfieldWithHom.exists_maximal_subfieldWithHom

added theorem lift.SubfieldWithHom.le_def

added theorem lift.SubfieldWithHom.maximalSubfieldWithHom_eq_top

added theorem lift.SubfieldWithHom.maximalSubfieldWithHom_is_maximal

added theorem lift.SubfieldWithHom.maximal_subfieldWithHom_chain_bounded

added structure lift.SubfieldWithHom