Commit 2024-06-25 09:57 bf261378

View on Github →

Feat (NumberTheory/Ostrowski): Proof of the non-archimedean case of Ostrowski's Theorem (#14026) In this PR we prove that a non-archimedean non-trivial absolute value on the rational is equivalent to a padic one. Main result

theorem mulRingNorm_equiv_padic_of_bounded :
    ∃! p, ∃ (hp : Fact (Nat.Prime p)), MulRingNorm.equiv f (mulRingNorm_padic p)

David Kurniadi Angdinata dka31@cantab.ac.uk Laura Capuano laura.capuano@uniroma3.it Nirvana Coppola nirvanac93@gmail.com María Inés de Frutos Fernández maria.defrutos@uam.es Sam van Gool vangool@irif.fr Silvain Rideau-Kikuchi silvain.rideau-kikuchi@ens.fr Amos Turchet amos.turchet@uniroma3.it Francesco Veneziano veneziano@dima.unige.it

Estimated changes

Modified Mathlib/NumberTheory/Ostrowski.lean

deleted theorem Rat.MulRingNorm.eq_on_Nat_iff_eq

deleted theorem Rat.MulRingNorm.eq_on_Nat_iff_eq_on_Int

added theorem Rat.MulRingNorm.eq_on_nat_iff_eq

added theorem Rat.MulRingNorm.eq_on_nat_iff_eq_on_Int

deleted theorem Rat.MulRingNorm.equiv_on_Nat_iff_equiv

added theorem Rat.MulRingNorm.equiv_on_nat_iff_equiv

added theorem Rat.MulRingNorm.exists_minimal_nat_zero_lt_mulRingNorm_lt_one

added theorem Rat.MulRingNorm.exists_pos_mulRingNorm_eq_pow_neg

added theorem Rat.MulRingNorm.is_prime_of_minimal_nat_zero_lt_mulRingNorm_lt_one

added theorem Rat.MulRingNorm.mulRingNorm_eq_one_of_not_dvd

added theorem Rat.MulRingNorm.mulRingNorm_eq_padic_norm

added theorem Rat.MulRingNorm.mulRingNorm_equiv_padic_of_bounded

added def Rat.MulRingNorm.mulRingNorm_padic