one_le_norm_A_of_ne_zero — Mathlib

English

Let A be a nonzero integer matrix. Its sup norm is at least 1.

Русский

Пусть A — ненулевая целочисленная матрица. Норма-суперсумма не меньше 1.

LaTeX

$$1 \\le \\|A\\|, \\quad \\text{when } A \\neq 0$$

Lean4

/-- The sup norm of a non-zero integer matrix is at least one -/
theorem one_le_norm_A_of_ne_zero (hA : A ≠ 0) : 1 ≤ ‖A‖ :=
  by
  by_contra! h
  apply hA
  ext i j
  simp only [zero_apply]
  rw [norm_lt_iff Real.zero_lt_one] at h
  specialize h i j
  rw [Int.norm_eq_abs] at h
  norm_cast at h
  exact Int.abs_lt_one_iff.1 h

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