A propagation prime coprime to a quadratic seed is odd

Proved

HorizontalPadicL.prime_ne_two_of_quadraticSeed

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

dirichlet-charactersmodular-formsnumber-theoryp-adic-l-functions

If the seed character has order two and its order is coprime to the propagation prime p, then p is not two. This supplies the odd-prime hypothesis automatically in the deduction of Corollary 5.17.

Preamble

import Definitions.Def_KN_SeededHorizontalPadicLFunctionV3

set_option autoImplicit false

Formal statement

namespace HorizontalPadicL

/-- A prime used to propagate from a quadratic seed is automatically odd when
the seed order is required to be coprime to that prime. -/
theorem prime_ne_two_of_quadraticSeed
    {p : ℕ} [Fact p.Prime]
    (η : DirichletCharacterWithLevel)
    (hηorder : orderOf η.2 = 2)
    (horderCoprime : Nat.Coprime (orderOf η.2) p) :
    p ≠ 2 := by
  sorry

end HorizontalPadicL

Source

Elementary consequence of coprimality; used in Kriz--Nordentoft, Corollary 5.17.

View graph