Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-20 04:23 035bd249

View on Github →

refactor(field_theory/algebraic_closure): Move construction of algebraic closure and lemmas about alg closed fields into seperate files. (#9265)

Estimated changes

Modified src/analysis/complex/polynomial.lean

Modified src/category_theory/preadditive/schur.lean

Created src/field_theory/is_alg_closed/algebraic_closure.lean

added theorem algebraic_closure.adjoin_monic.algebra_map

added theorem algebraic_closure.adjoin_monic.exists_root

added theorem algebraic_closure.adjoin_monic.is_integral

added def algebraic_closure.adjoin_monic

added theorem algebraic_closure.algebra_map_def

added theorem algebraic_closure.coe_to_step_of_le

added def algebraic_closure.eval_X_self

added theorem algebraic_closure.exists_of_step

added theorem algebraic_closure.exists_root

added theorem algebraic_closure.is_algebraic

added theorem algebraic_closure.le_max_ideal

added def algebraic_closure.max_ideal

added def algebraic_closure.monic_irreducible

added def algebraic_closure.of_step

added def algebraic_closure.of_step_hom

added theorem algebraic_closure.of_step_succ

added def algebraic_closure.span_eval

added theorem algebraic_closure.span_eval_ne_top

added theorem algebraic_closure.step.is_integral

added def algebraic_closure.step

added def algebraic_closure.step_aux

added def algebraic_closure.to_adjoin_monic

added def algebraic_closure.to_splitting_field

added theorem algebraic_closure.to_splitting_field_eval_X_self

added def algebraic_closure.to_step_of_le

added theorem algebraic_closure.to_step_succ.exists_root

added def algebraic_closure.to_step_succ

added def algebraic_closure.to_step_zero

added def algebraic_closure

Renamed src/field_theory/algebraic_closure.lean to src/field_theory/is_alg_closed/basic.lean

deleted theorem algebraic_closure.adjoin_monic.algebra_map

deleted theorem algebraic_closure.adjoin_monic.exists_root

deleted theorem algebraic_closure.adjoin_monic.is_integral

deleted def algebraic_closure.adjoin_monic

deleted theorem algebraic_closure.algebra_map_def

deleted theorem algebraic_closure.coe_to_step_of_le

deleted def algebraic_closure.eval_X_self

deleted theorem algebraic_closure.exists_of_step

deleted theorem algebraic_closure.exists_root

deleted theorem algebraic_closure.is_algebraic

deleted theorem algebraic_closure.le_max_ideal

deleted def algebraic_closure.max_ideal

deleted def algebraic_closure.monic_irreducible

deleted def algebraic_closure.of_step

deleted def algebraic_closure.of_step_hom

deleted theorem algebraic_closure.of_step_succ

deleted def algebraic_closure.span_eval

deleted theorem algebraic_closure.span_eval_ne_top

deleted theorem algebraic_closure.step.is_integral

deleted def algebraic_closure.step

deleted def algebraic_closure.step_aux

deleted def algebraic_closure.to_adjoin_monic

deleted def algebraic_closure.to_splitting_field

deleted theorem algebraic_closure.to_splitting_field_eval_X_self

deleted def algebraic_closure.to_step_of_le

deleted theorem algebraic_closure.to_step_succ.exists_root

deleted def algebraic_closure.to_step_succ

deleted def algebraic_closure.to_step_zero

deleted def algebraic_closure

deleted def is_alg_closed.lift

deleted def lift.subfield_with_hom.maximal_subfield_with_hom

Modified src/field_theory/primitive_element.lean

Modified src/linear_algebra/eigenspace.lean

Modified src/ring_theory/nullstellensatz.lean

Modified src/ring_theory/trace.lean