Commit 2023-06-19 08:58 2f34d0b2

View on Github →

feat: port FieldTheory.IsAlgClosed.AlgebraicClosure (#5074)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

added theorem AlgebraicClosure.AdjoinMonic.algebraMap

added theorem AlgebraicClosure.AdjoinMonic.exists_root

added theorem AlgebraicClosure.AdjoinMonic.isIntegral

added def AlgebraicClosure.AdjoinMonic

added def AlgebraicClosure.MonicIrreducible

added theorem AlgebraicClosure.Step.isIntegral

added theorem AlgebraicClosure.Step.succ

added theorem AlgebraicClosure.Step.zero

added def AlgebraicClosure.Step

added theorem AlgebraicClosure.algebraMap_def

added theorem AlgebraicClosure.coe_toStepOfLE

added def AlgebraicClosure.evalXSelf

added theorem AlgebraicClosure.exists_ofStep

added theorem AlgebraicClosure.exists_root

added theorem AlgebraicClosure.isAlgebraic

added theorem AlgebraicClosure.le_maxIdeal

added def AlgebraicClosure.maxIdeal

added def AlgebraicClosure.ofStep

added def AlgebraicClosure.ofStepHom

added theorem AlgebraicClosure.ofStep_succ

added def AlgebraicClosure.spanEval

added theorem AlgebraicClosure.spanEval_ne_top

added def AlgebraicClosure.stepAux

added def AlgebraicClosure.toAdjoinMonic

added def AlgebraicClosure.toSplittingField

added theorem AlgebraicClosure.toSplittingField_evalXSelf

added def AlgebraicClosure.toStepOfLE

added theorem AlgebraicClosure.toStepSucc.exists_root

added def AlgebraicClosure.toStepSucc

added def AlgebraicClosure.toStepZero

added def AlgebraicClosure