gaussSum_eq_zero_of_isPrimitive_of_not_isPrimitive

English

If χ is primitive but e is not primitive, then gaussSum χ e = 0.

Русский

Если χ примитивен, но e не примитивен, то gaussSum χ e = 0.

LaTeX

$$$\\text{gaussSum\\_eq\\_zero\\_of\\_isPrimitive\\_of\\_not\\_isPrimitive}: χ.IsPrimitive \\rightarrow ¬ e.IsPrimitive \\rightarrow gaussSum χ e = 0.$$$

Lean4

/-- If `χ` is primitive, but `e` is not, then `gaussSum χ e = 0`. -/
theorem gaussSum_eq_zero_of_isPrimitive_of_not_isPrimitive [IsDomain R] {χ : DirichletCharacter R N}
    (hχ : IsPrimitive χ) (he : ¬IsPrimitive e) : gaussSum χ e = 0 :=
  by
  contrapose! hχ
  rcases e.exists_divisor_of_not_isPrimitive he with ⟨d, hd₁, hd₂, hed⟩
  have : χ.conductor ≤ d := Nat.sInf_le <| factorsThrough_of_gaussSum_ne_zero e hd₁ hed hχ
  exact (this.trans_lt hd₂).ne

Похожие утверждения