Theorem DenseRange.addChar_eq_of_apply_one_eq

Modification history

2025-04-23 11:46

Mathlib/Topology/Algebra/Monoid/AddChar.lean

feat(NumberTheory/Padics): leftovers from PR 24141 (#24310) …

Deleted DenseRange.addChar_eq_of_apply_one_eq View on Github →

2025-04-23 09:35

Mathlib/Topology/Algebra/Monoid/AddChar.lean

feat(NumberTheory/Padics): parametrization of cts add chars of Z_[p] (#24141) …

Added DenseRange.addChar_eq_of_apply_one_eq View on Github →