English
The p-adic integers ℤ_p form the domain of fractions with ℚ_p as its field of fractions; i.e., ℚ_p is the fraction field of ℤ_p.
Русский
p-адические целые числа ℤ_p являются кольцом дробей, а их поля дробей равно ℚ_p.
LaTeX
$$IsFractionRing(ℤ_[p], ℚ_[p]).$$
Lean4
instance isFractionRing : IsFractionRing ℤ_[p] ℚ_[p]
where
map_units := fun ⟨x, hx⟩ => by
rwa [algebraMap_apply, isUnit_iff_ne_zero, PadicInt.coe_ne_zero, ← mem_nonZeroDivisors_iff_ne_zero]
surj
x := by
by_cases hx : ‖x‖ ≤ 1
· use (⟨x, hx⟩, 1)
rw [Submonoid.coe_one, map_one, mul_one, PadicInt.algebraMap_apply, Subtype.coe_mk]
· set n := Int.toNat (-x.valuation) with hn
have hn_coe : (n : ℤ) = -x.valuation := by
rw [hn, Int.toNat_of_nonneg]
rw [Right.nonneg_neg_iff]
rw [Padic.norm_le_one_iff_val_nonneg, not_le] at hx
exact hx.le
set a := x * (p : ℚ_[p]) ^ n with ha
have ha_norm : ‖a‖ = 1 :=
by
have hx : x ≠ 0 := by
intro h0
rw [h0, norm_zero] at hx
exact hx zero_le_one
rw [ha, padicNormE.mul, Padic.norm_p_pow, Padic.norm_eq_zpow_neg_valuation hx, ← zpow_add', hn_coe, neg_neg,
neg_add_cancel, zpow_zero]
exact Or.inl (Nat.cast_ne_zero.mpr (NeZero.ne p))
use (⟨a, le_of_eq ha_norm⟩, ⟨(p ^ n : ℤ_[p]), mem_nonZeroDivisors_iff_ne_zero.mpr (NeZero.ne _)⟩)
simp only [a, map_pow, map_natCast, algebraMap_apply]
exists_of_eq := by
simp_rw [algebraMap_apply, Subtype.coe_inj]
exact fun h => ⟨1, by rw [h]⟩
