feat(Wikipedia): add ERH for Dedekind zeta

[Robertboy18]

Pushed #2376 by adding a Lean statement of the ERH for Dedekind zeta functions, using Mathlib’s NumberField.dedekindZeta (zeros in 0 < Re(s) < 1 lie on Re(s) = 1/2)! Let me know what changes are needed.

[Paul-Lez]

Thanks for the contribution! One minor comment - I'll take a look at the maths later on:)

[Paul-Lez]

Generally, we tend to use the file name for the namespace (or something similar), so here I'd suggest the following:

Suggested change

	namespace ERH
	namespace ExtendedRiemannHypothesis

[Robertboy18]

Good catch! updated the namespace to ExtendedRiemannHypothesis to match the file name. Thanks!

[smmercuri]

In #2378 it is proposed that we use the file Wikipedia/RiemannHypothesis.lean for both RH and GRH, so I think we should use it also for ERH. I'd suggest renaming the file in this PR to RiemannHypothesis.lean

[Robertboy18]

Thanks for the review and I agree! That was totally my bad I didn't check more - I had just formalized what i thought was good from one of my ugrad classes concepts and should have done more literature study!

I’ve strengthened the main Lean statement to quantify over all zeros of ζ_K, excluding the trivial zeros (via hs_nontrivial, see trivialZeros) and excluding s = 1 (the pole), so it now rules out zeros like 1.25 + 100i as well.

I also kept the “critical strip” formulation as a derived lemma and added clearer references/comments.

Thanks!