ℤ as a normed group

instance Int.instNormedAddCommGroup : NormedAddCommGroup ℤ

Equations

• Int.instNormedAddCommGroup = NormedAddCommGroup.mk Int.instNormedAddCommGroup.proof_1

theorem Int.norm_cast_real (m : ℤ) : ‖↑m‖ = ‖m‖

theorem Int.norm_eq_abs (n : ℤ) : ‖n‖ = |↑n|

@[simp]

theorem Int.norm_natCast (n : ℕ) : ‖↑n‖ = ↑n

theorem NNReal.natCast_natAbs (n : ℤ) : ↑n.natAbs = ‖n‖₊

theorem Int.abs_le_floor_nnreal_iff (z : ℤ) (c : NNReal) : |z| ≤ ↑⌊c⌋₊ ↔ ‖z‖₊ ≤ c

theorem norm_zpow_le_mul_norm {α : Type u_1} [SeminormedCommGroup α] (n : ℤ) (a : α) : ‖a ^ n‖ ≤ ‖n‖ * ‖a‖

theorem norm_zsmul_le {α : Type u_1} [SeminormedAddCommGroup α] (n : ℤ) (a : α) : ‖n • a‖ ≤ ‖n‖ * ‖a‖

theorem nnnorm_zpow_le_mul_norm {α : Type u_1} [SeminormedCommGroup α] (n : ℤ) (a : α) : ‖a ^ n‖₊ ≤ ‖n‖₊ * ‖a‖₊

theorem nnnorm_zsmul_le {α : Type u_1} [SeminormedAddCommGroup α] (n : ℤ) (a : α) : ‖n • a‖₊ ≤ ‖n‖₊ * ‖a‖₊