abs_le_left_of_norm — Mathlib

English

For integers m,n, the absolute value of n is bounded by the norm of the pair [n,m].

Русский

Для целых m,n, |n| не превосходит норму пары [n,m].

LaTeX

$$ |n| ≤ ‖![n,m]‖$$

Lean4

theorem abs_le_left_of_norm (m n : ℤ) : |n| ≤ ‖![n, m]‖ :=
  by
  simp only [EisensteinSeries.norm_eq_max_natAbs, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one,
    Matrix.cons_val_fin_one, Nat.cast_max, le_sup_iff]
  left
  rw [Int.abs_eq_natAbs]
  exact Preorder.le_refl _

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