p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ ↑(↑padicNormE (q + r)) ≤ max ↑(↑padicNormE q) ↑(↑padicNormE r)
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ ‖q + r‖ ≤ max ‖q‖ ‖r‖
dsimp [norm]
no goals
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ ↑(↑padicNormE (q + r)) ≤ max ↑(↑padicNormE q) ↑(↑padicNormE r)
exact_mod_cast nonarchimedean' _ _