Commit 2024-10-21 09:28 26449dce
View on Github →feat(NumberTheory/Ostrowski): Ostrowski's Theorem for the rationals (#17138) We complete the proof of the Archimedean case of Ostrowski's Theorem for the rational numbers:
theorem mulRingNorm_equiv_standard_of_unbounded (notbdd: ¬ ∀ (n : ℕ), f n ≤ 1) :
MulRingNorm.equiv f mulRingNorm_real
This concludes the proof of the theorem:
theorem mulRingNorm_equiv_standard_or_padic (f : MulRingNorm ℚ) (hf_nontriv : f ≠ 1) :
(MulRingNorm.equiv f mulRingNorm_real) ∨
∃! p, ∃ (hp : Fact (p.Prime)), MulRingNorm.equiv f (mulRingNorm_padic p)