Commit 2024-12-11 13:59 6e4ad6d7

View on Github →

chore: golf AlgebraicClosure construction using Isaacs (#19853) Also moves Polynomial.isRoot_of_isRoot_iff_dvd_derivative_mul to an earlier file.

Estimated changes

Modified Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

deleted theorem AlgebraicClosure.AdjoinMonic.algebraMap

deleted theorem AlgebraicClosure.AdjoinMonic.exists_root

deleted theorem AlgebraicClosure.AdjoinMonic.isIntegral

deleted def AlgebraicClosure.AdjoinMonic

deleted theorem AlgebraicClosure.Step.isIntegral

deleted theorem AlgebraicClosure.Step.succ

deleted theorem AlgebraicClosure.Step.zero

deleted def AlgebraicClosure.Step

deleted def AlgebraicClosure.algEquivAlgebraicClosureAux

deleted theorem AlgebraicClosure.coe_toStepOfLE

deleted def AlgebraicClosure.stepAux

deleted def AlgebraicClosure.toAdjoinMonic

deleted def AlgebraicClosure.toStepOfLE

deleted theorem AlgebraicClosure.toStepSucc.exists_root

deleted def AlgebraicClosure.toStepSucc

deleted def AlgebraicClosure.toStepZero

deleted theorem AlgebraicClosureAux.exists_ofStep

deleted theorem AlgebraicClosureAux.exists_root

deleted theorem AlgebraicClosureAux.instIsAlgClosed

deleted theorem AlgebraicClosureAux.isAlgClosure

deleted def AlgebraicClosureAux.ofStep

deleted def AlgebraicClosureAux.ofStepHom

deleted theorem AlgebraicClosureAux.ofStep_succ

deleted def AlgebraicClosureAux

deleted theorem Polynomial.isRoot_of_isRoot_iff_dvd_derivative_mul

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

added theorem Polynomial.isRoot_of_isRoot_iff_dvd_derivative_mul