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)

Estimated changes