Commit 2025-07-07 13:51 19d36011

View on Github →

feat(NumberTheory/Padics/Complex.lean): add the padic complex numbers (#26675) We define the field of p-adic complex numbers.

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Padics/Complex.lean

added theorem PadicAlgCl.coe_eq

added theorem PadicAlgCl.isAlgebraic

added theorem PadicAlgCl.isNonarchimedean

added theorem PadicAlgCl.norm_extends

added theorem PadicAlgCl.spectralNorm_eq

added theorem PadicAlgCl.valuation_coe

added theorem PadicAlgCl.valuation_def

added theorem PadicAlgCl.valuation_p

added theorem PadicComplex.coe_eq

added theorem PadicComplex.coe_natCast

added theorem PadicComplex.coe_zero

added theorem PadicComplex.isNonarchimedean

added theorem PadicComplex.nnnorm_extends

added theorem PadicComplex.norm_def

added theorem PadicComplex.norm_extends

added theorem PadicComplex.rankOne_hom_eq

added theorem PadicComplex.valuation_extends

added theorem PadicComplex.valuation_p

added theorem PadicComplexInt.integers

added def PadicComplexInt