ℤ as a normed group

@[instance_reducible]

instance Int.instNormedAddCommGroup : NormedAddCommGroup ℤ

Equations

• Int.instNormedAddCommGroup = { norm := fun (n : ℤ) => ‖↑n‖, toAddCommGroup := Int.instAddCommGroup, toMetricSpace := Int.instMetricSpace, dist_eq := ⋯ }

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

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

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‖₊

@[deprecated nnNorm_zpow_le_mul_norm (since := "2026-10-31")]

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

Alias of nnNorm_zpow_le_mul_norm.

@[deprecated nnNorm_zsmul_le (since := "2026-10-31")]

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

Alias of nnNorm_zsmul_le.