def ArithFunc.IsDirichletCharModulus (f : ArithFunc) (m : ℕ) : Prop

theorem ArithFunc.IsPeriodic.iterate {f : ArithFunc} {m : ℕ} (hf : f.IsPeriodic m) (k n : ℕ) : f (n + m * k) = f n

theorem ArithFunc.IsPeriodic.of_dvd {f : ArithFunc} {m m' : ℕ} (hfm : f.IsPeriodic m) (h : m ∣ m') : f.IsPeriodic m'

theorem ArithFunc.IsPeriodic.eq_mod {f : ArithFunc} {m : ℕ} (hf_per : f.IsPeriodic m) (a : ℕ) : f a = f (a % m)

theorem ArithFunc.IsPeriodic.eq_of_modEq {f : ArithFunc} {m : ℕ} (hf_per : f.IsPeriodic m) {a b : ℕ} (h : a ≡ b [MOD m]) : f a = f b

theorem ArithFunc.period_pos' {f : ArithFunc} (hf : ∃ (m : ℕ), 0 < m ∧ f.IsPeriodic m) : 0 < f.period

theorem ArithFunc.period_isPeriodic' {f : ArithFunc} (hf : ∃ (m : ℕ), 0 < m ∧ f.IsPeriodic m) : f.IsPeriodic f.period

theorem ArithFunc.period_min' {f : ArithFunc} {k : ℕ} (hf : ∃ (m : ℕ), 0 < m ∧ f.IsPeriodic m) (hk : 0 < k ∧ f.IsPeriodic k) : f.period ≤ k

theorem ArithFunc.period_dvd_of_isPeriodic {f : ArithFunc} {m : ℕ} (hm : 0 < m) (hfm : f.IsPeriodic m) : f.period ∣ m

theorem ArithFunc.nonzero_imp_coprime {f : ArithFunc} {m : ℕ} (hf_tm : f.IsTotallyMultiplicative) (hm_pos : 0 < m) (hf_per : f.IsPeriodic m) (hf_min : ∀ (k : ℕ), 0 < k → f.IsPeriodic k → m ≤ k) {n : ℕ} (hn : f n ≠ 0) : m.Coprime n

theorem ArithFunc.coprime_imp_nonzero {f : ArithFunc} {m : ℕ} (hf_tm : f.IsTotallyMultiplicative) (hm_pos : 0 < m) (hf_per : f.IsPeriodic m) {n : ℕ} (hcop : m.Coprime n) : f n ≠ 0

theorem dvd_pow_of_primeFactors_subset {m m' : ℕ} (hm' : m' ≠ 0) (hsub : m'.primeFactors ⊆ m.primeFactors) : ∃ (k : ℕ), m' ∣ m ^ k

theorem ArithFunc.lemma_18_8 {f : ArithFunc} {m : ℕ} (hf_tm : f.IsTotallyMultiplicative) (hm_pos : 0 < m) (hf_per : f.IsPeriodic m) (hf_min : f.period = m) (m' : ℕ) (hm'_pos : 0 < m') : f.IsDirichletCharModulus m' ↔ m ∣ m' ∧ ∃ (k : ℕ), m' ∣ m ^ k