Commit 2023-09-04 17:05 174c56b3

View on Github →

chore: redefine AlgebraicClosure to make certain instance diagrams commute (#6734) A similar trick to the trick used in #4891 makes all the required type class diagrams commute. I also added instances for CharP and CharZero and tests for the instance diagrams.

Estimated changes

Modified Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

added def AlgebraicClosure.algEquivAlgebraicClosureAux

deleted theorem AlgebraicClosure.algebraMap_def

deleted theorem AlgebraicClosure.exists_ofStep

deleted theorem AlgebraicClosure.exists_root

modified theorem AlgebraicClosure.isAlgebraic

deleted def AlgebraicClosure.ofStep

deleted def AlgebraicClosure.ofStepHom

deleted theorem AlgebraicClosure.ofStep_succ

added theorem AlgebraicClosureAux.exists_ofStep

added theorem AlgebraicClosureAux.exists_root

added theorem AlgebraicClosureAux.instIsAlgClosed

added theorem AlgebraicClosureAux.isAlgClosure

added theorem AlgebraicClosureAux.isAlgebraic

added def AlgebraicClosureAux.ofStep

added def AlgebraicClosureAux.ofStepHom

added theorem AlgebraicClosureAux.ofStep_succ

added def AlgebraicClosureAux

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

added theorem IsAlgClosed.of_ringEquiv