Theorem PadicAlgCl.norm_extends

Modification history

2026-03-27 16:17
Mathlib/NumberTheory/Padics/Complex.lean
chore(IsAlgClosed/AlgebraicClosure): clean up instances (#37257) …
Modified PadicAlgCl.norm_extendsView on Github →
2025-07-07 13:51
Mathlib/NumberTheory/Padics/Complex.lean
feat(NumberTheory/Padics/Complex.lean): add the padic complex numbers (#26675) …
Added PadicAlgCl.norm_extendsView on Github →