Arithmetic of primitive products of Dirichlet characters

Proved

HorizontalPadicL.primitiveProductArithmetic

by davidloeffler · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

dirichlet-charactersnumber-theoryp-adic-l-functions

Primitive-product arithmetic for coprime conductors and coprime orders, including cancellation on primitive characters. This is standard Dirichlet character theory and involves no modular forms or nonvanishing theorem.

Preamble

import Definitions.Def_KN_PrimePowerPropagation

set_option autoImplicit false
noncomputable section
open scoped BigOperators

Formal statement

namespace HorizontalPadicL

/-- Primitive-product arithmetic for coprime conductors and coprime orders,
including cancellation on primitive characters. This is standard Dirichlet
character theory and involves no modular forms or nonvanishing theorem. -/
theorem primitiveProductArithmetic : PrimitiveProductArithmetic := by
  sorry

end HorizontalPadicL

Source

Kriz--Nordentoft, Horizontal p-adic L-functions, https://arxiv.org/pdf/2310.20678, Section 2.3.3, Lemma 5.7, Theorem 5.9 and Corollary 5.10.

View graph