Theorem PadicComplex.isNonarchimedean

Modification history

2026-02-23 03:56

Mathlib/NumberTheory/Padics/Complex.lean

chore: golf proofs (#35244) …

Modified PadicComplex.isNonarchimedean View on Github →

2025-07-07 13:51

Mathlib/NumberTheory/Padics/Complex.lean

feat(NumberTheory/Padics/Complex.lean): add the padic complex numbers (#26675) …

Added PadicComplex.isNonarchimedean View on Github →