feat(analysis/normed_space/basic): int.norm_eq_abs (#8117)

leanprover-community · Jun 29, 2021 · 23ee7ea · 23ee7ea
1 parent d249e53
commit 23ee7ea
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean
@@ -1305,6 +1305,8 @@ instance : normed_comm_ring ℤ :=
 
 @[norm_cast] lemma int.norm_cast_real (m : ℤ) : ∥(m : ℝ)∥ = ∥m∥ := rfl
 
+lemma int.norm_eq_abs (n : ℤ) : ∥n∥ = abs n := rfl
+
 lemma nnreal.coe_nat_abs (n : ℤ) : (n.nat_abs : ℝ≥0) = ∥n∥₊ :=
 nnreal.eq $ calc ((n.nat_abs : ℝ≥0) : ℝ)
                = (n.nat_abs : ℤ) : by simp only [int.cast_coe_nat, nnreal.coe_nat_cast]