Skip to content

Commit

Permalink
Fix typo in docstring
Browse files Browse the repository at this point in the history
Co-authored-by: David Loeffler <[email protected]>
  • Loading branch information
MichaelStollBayreuth and loefflerd authored Oct 28, 2024
1 parent 1b424cf commit 37a82ea
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/NumberTheory/LSeries/Dirichlet.lean
Original file line number Diff line number Diff line change
Expand Up @@ -106,7 +106,7 @@ local notation (name := Dchar_one) "χ₁" => (1 : DirichletCharacter ℂ 1)
namespace DirichletCharacter

open ArithmeticFunction in
/-- The arihmetic function associated to a Dirichlet character is multiplicative. -/
/-- The arithmetic function associated to a Dirichlet character is multiplicative. -/
lemma isMultiplicative_toArithmeticFunction {N : ℕ} {R : Type*} [CommMonoidWithZero R]
(χ : DirichletCharacter R N) :
(toArithmeticFunction (χ ·)).IsMultiplicative := by
Expand Down

0 comments on commit 37a82ea

Please sign in to comment.