norm_le_norm_mul_left — Mathlib

English

For x ∈ ℤ[i] and y ∈ ℤ[i] with y ≠ 0, (norm x).natAbs ≤ (norm (x*y)).natAbs.

Русский

Для x ∈ ℤ[i] и y ∈ ℤ[i], y ≠ 0, верно (norm x).natAbs ≤ (norm (x*y)).natAbs.

LaTeX

$$$ (\operatorname{norm}(x)).natAbs \le (\operatorname{norm}(x \cdot y)).natAbs $$$

Lean4

theorem norm_le_norm_mul_left (x : ℤ[i]) {y : ℤ[i]} (hy : y ≠ 0) : (norm x).natAbs ≤ (norm (x * y)).natAbs :=
  by
  rw [Zsqrtd.norm_mul, Int.natAbs_mul]
  exact
    le_mul_of_one_le_right (Nat.zero_le _)
      (Int.ofNat_le.1
        (by
          rw [abs_natCast_norm]
          exact Int.add_one_le_of_lt (norm_pos.2 hy)))

Похожие утверждения