Theorem PadicAlgCl.valuation_coe

Modification history

2026-05-29 13:23

Mathlib/NumberTheory/Padics/Complex.lean

chore: bump toolchain to v4.31.0-rc1 (#39980)

Modified PadicAlgCl.valuation_coe 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 PadicAlgCl.valuation_coe View on Github →