Theorem PadicInt.coe_addChar_of_value_at_one

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