chore(number_theory/padics): fix lemma names and golf (#17798)

The `norm_p_pow` lemma was actually a lemma about `zpow`. This renames it add adds the missing lemma about pow.

This also uses a nicer algebra instance that agrees with the subring definition, although it probably doesn't matter anywhere.

src/number_theory/padics/padic_integers.lean

@@ -114,6 +114,8 @@ instance : has_one ℤ_[p] := ⟨⟨1, by norm_num⟩⟩
 lemma coe_eq_zero (z : ℤ_[p]) : (z : ℚ_[p]) = 0 ↔ z = 0 :=
 by rw [← coe_zero, subtype.coe_inj]
 
+lemma coe_ne_zero (z : ℤ_[p]) : (z : ℚ_[p]) ≠ 0 ↔ z ≠ 0 := z.coe_eq_zero.not
+
 instance : add_comm_group ℤ_[p] :=
 (by apply_instance : add_comm_group (subring p))
 
@@ -534,16 +536,14 @@ end dvr
 
 section fraction_ring
 
-instance algebra : algebra ℤ_[p] ℚ_[p] := ring_hom.to_algebra (padic_int.coe.ring_hom)
+instance algebra : algebra ℤ_[p] ℚ_[p] := algebra.of_subring (subring p)
 
 @[simp] lemma algebra_map_apply (x : ℤ_[p]) : algebra_map ℤ_[p] ℚ_[p] x = x := rfl
 
 instance is_fraction_ring : is_fraction_ring ℤ_[p] ℚ_[p] :=
 { map_units := λ ⟨x, hx⟩,
-  begin
-    rw [set_like.coe_mk, algebra_map_apply, is_unit_iff_ne_zero, ne.def, padic_int.coe_eq_zero],
-    exact mem_non_zero_divisors_iff_ne_zero.mp hx,
-  end,
+  by rwa [set_like.coe_mk, algebra_map_apply, is_unit_iff_ne_zero, padic_int.coe_ne_zero,
+      ←mem_non_zero_divisors_iff_ne_zero],
   surj := λ x,
   begin
     by_cases hx : ‖ x ‖ ≤ 1,
@@ -561,8 +561,8 @@ instance is_fraction_ring : is_fraction_ring ℤ_[p] ℚ_[p] :=
         { intro h0,
           rw [h0, norm_zero] at hx,
           exact hx (zero_le_one) },
-        rw [ha, padic_norm_e.mul, ← zpow_coe_nat, padic_norm_e.norm_p_pow,
-          padic.norm_eq_pow_val hx, ← zpow_add' , hn_coe, neg_neg, add_left_neg, zpow_zero],
+        rw [ha, padic_norm_e.mul, padic_norm_e.norm_p_pow,
+          padic.norm_eq_pow_val hx, ← zpow_add', hn_coe, neg_neg, add_left_neg, zpow_zero],
         exact or.inl (nat.cast_ne_zero.mpr (ne_zero.ne p)), },
       use (⟨a, le_of_eq ha_norm⟩,
         ⟨(p^n : ℤ_[p]), mem_non_zero_divisors_iff_ne_zero.mpr (ne_zero.ne _)⟩),

src/number_theory/padics/padic_numbers.lean

@@ -726,8 +726,11 @@ begin
   exact_mod_cast hp.1.one_lt
 end
 
-@[simp] lemma norm_p_pow (n : ℤ) : ‖(p ^ n : ℚ_[p])‖ = p ^ -n :=
-by rw [norm_zpow, norm_p]; field_simp
+@[simp] lemma norm_p_zpow (n : ℤ) : ‖(p ^ n : ℚ_[p])‖ = p ^ -n :=
+by rw [norm_zpow, norm_p, zpow_neg, inv_zpow]
+
+@[simp] lemma norm_p_pow (n : ℕ) : ‖(p ^ n : ℚ_[p])‖ = p ^ (-n : ℤ) :=
+by rw [←norm_p_zpow, zpow_coe_nat]
 
 instance : nontrivially_normed_field ℚ_[p] :=
 { non_trivial := ⟨p⁻¹, begin