Theorem PadicInt.continuousAddCharEquiv_of_norm_mul_symm_apply

Modification history

2025-04-23 09:35
Mathlib/NumberTheory/Padics/AddChar.lean
feat(NumberTheory/Padics): parametrization of cts add chars of Z_[p] (#24141) …
Added PadicInt.continuousAddCharEquiv_of_norm_mul_symm_applyView on Github →