HepLean Documentation

Mathlib.Analysis.Normed.Group.Int

ℤ as a normed group #

theorem Int.norm_eq_abs (n : ) :
n = |n|
@[simp]
theorem Int.norm_natCast (n : ) :
n = n
@[deprecated Int.norm_natCast]
theorem Int.norm_coe_nat (n : ) :
n = n

Alias of Int.norm_natCast.

theorem NNReal.natCast_natAbs (n : ) :
n.natAbs = n‖₊
theorem norm_zpow_le_mul_norm {α : Type u_1} [SeminormedCommGroup α] (n : ) (a : α) :
theorem norm_zsmul_le {α : Type u_1} [SeminormedAddCommGroup α] (n : ) (a : α) :