Commit 2025-08-15 22:00 671301c4

View on Github →

feat(NumberTheory/Padics): {Int,Rat}.padicValuation (#27667) padicVal{Int,Rat} in Valuation form, sending to ℤᵐ⁰ We didn't have a valuation that mentioned Rat and Valuation together before. On the way to show that ℚ_[p] (resp. ℤ_[p]) is equivalent to Completion (WithVal v) for the v defined here

Estimated changes

Modified Mathlib/NumberTheory/Padics/PadicNumbers.lean

added def Int.padicValuation

added theorem Int.padicValuation_eq_one_iff

added theorem Int.padicValuation_eq_zero_iff

added theorem Int.padicValuation_le_one

added theorem Int.padicValuation_lt_one_iff

added theorem Int.padicValuation_self

added theorem Padic.comap_mulValuation_eq_int_padicValuation

added theorem Padic.comap_mulValuation_eq_padicValuation

added theorem Padic.norm_eq_zpow_log_mulValuation

added def Rat.padicValuation

added theorem Rat.padicValuation_cast

added theorem Rat.padicValuation_eq_zero_iff

added theorem Rat.padicValuation_le_one_iff

added theorem Rat.padicValuation_self

Modified Mathlib/NumberTheory/Padics/PadicVal/Basic.lean

added theorem padicValInt.eq_zero_iff