Theorem PadicInt.addChar_of_value_at_one_def

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.addChar_of_value_at_one_defView on Github →