p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
⊢ valuation (x * y) = valuation x + valuation y
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
⊢ valuation (x * y) = valuation x + valuation y
have h_norm : ‖x * y‖ = ‖x‖ * ‖y‖ := norm_mul x y
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : ↑p ≠ 1
⊢ valuation (x * y) = valuation x + valuation y
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
⊢ valuation (x * y) = valuation x + valuation y
have hp_ne_one : (p : ℝ) ≠ 1 := by
  rw [← Nat.cast_one, Ne.def, Nat.cast_inj]
  exact Nat.Prime.ne_one hp.elim
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : ↑p ≠ 1
hp_pos : 0 < ↑p
⊢ valuation (x * y) = valuation x + valuation y
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : ↑p ≠ 1
⊢ valuation (x * y) = valuation x + valuation y
have hp_pos : (0 : ℝ) < p := by
  rw [← Nat.cast_zero, Nat.cast_lt]
  exact Nat.Prime.pos hp.elim
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : valuation (x * y) = valuation x + valuation y
hp_ne_one : ↑p ≠ 1
hp_pos : 0 < ↑p
⊢ valuation (x * y) = valuation x + valuation y
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : ↑p ≠ 1
hp_pos : 0 < ↑p
⊢ valuation (x * y) = valuation x + valuation y
rw [norm_eq_pow_val hx, norm_eq_pow_val hy, norm_eq_pow_val (mul_ne_zero hx hy), ←
  zpow_add₀ (ne_of_gt hp_pos), zpow_inj hp_pos hp_ne_one, ← neg_add, neg_inj] at h_norm
no goals
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : valuation (x * y) = valuation x + valuation y
hp_ne_one : ↑p ≠ 1
hp_pos : 0 < ↑p
⊢ valuation (x * y) = valuation x + valuation y
exact h_norm
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
⊢ ¬p = 1
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
⊢ ↑p ≠ 1
rw [← Nat.cast_one, Ne.def, Nat.cast_inj]
no goals
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
⊢ ¬p = 1
exact Nat.Prime.ne_one hp.elim
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : ↑p ≠ 1
⊢ 0 < p
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : ↑p ≠ 1
⊢ 0 < ↑p
rw [← Nat.cast_zero, Nat.cast_lt]
no goals
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : ↑p ≠ 1
⊢ 0 < p
exact Nat.Prime.pos hp.elim