appease linter

leanprover-community · Oct 27, 2024 · 2cdf288 · 2cdf288
1 parent 4e34d1e
commit 2cdf288
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/NumberTheory/LSeries/Dirichlet.lean b/Mathlib/NumberTheory/LSeries/Dirichlet.lean
@@ -109,7 +109,7 @@ open ArithmeticFunction in
 /-- The arihmetic function associated to a Dirichlet character is multiplicative. -/
 lemma isMultiplicative_toArithmeticFunction {N : ℕ} {R : Type*} [CommMonoidWithZero R]
     (χ : DirichletCharacter R N) :
-    (toArithmeticFunction (χ .)).IsMultiplicative := by
+    (toArithmeticFunction (χ ·)).IsMultiplicative := by
   refine IsMultiplicative.iff_ne_zero.mpr ⟨?_, fun {m} {n} hm hn _ ↦ ?_⟩
   · simp only [toArithmeticFunction, coe_mk, one_ne_zero, ↓reduceIte, Nat.cast_one, map_one]
   · simp only [toArithmeticFunction, coe_mk, mul_eq_zero, hm, hn, false_or, Nat.cast_mul, map_mul,