Commit 2026-03-27 16:17 37fa7783

View on Github →

chore(IsAlgClosed/AlgebraicClosure): clean up instances (#37257) Clean up the instances on AlgebraicClosure.

Estimated changes

Modified Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

Modified Mathlib/NumberTheory/Padics/Complex.lean

modified theorem PadicAlgCl.norm_extends