English
For A ∈ reps m, each entry A_{ij} belongs to the interval [ -|m|, |m| ].
Русский
Для A ∈ reps m каждый элемент A_{ij} лежит в интервале [ -|m|, |m| ].
LaTeX
$$$A \in \text{reps}(m)\Rightarrow A_{ij} \in [-|m|,|m|]$ for all i,j.$$
Lean4
/-- An auxiliary result bounding the size of the entries of the representatives in `reps` -/
theorem reps_entries_le_m' {A : Δ m} (h : A ∈ reps m) (i j : Fin 2) : A.1 i j ∈ Finset.Icc (-|m|) |m| :=
by
suffices |A.1 i j| ≤ |m| from Finset.mem_Icc.mpr <| abs_le.mp this
obtain ⟨h10, h00, h01, h11⟩ := h
have h1 : 0 < |A.1 1 1| := (abs_nonneg _).trans_lt h11
have h2 : 0 < |A.1 0 0| := abs_pos.mpr h00.ne'
fin_cases i <;> fin_cases j
· simpa only [← abs_mul, A_c_eq_zero h10] using (le_mul_iff_one_le_right h2).mpr h1
· simpa only [← abs_mul, A_c_eq_zero h10] using h11.le.trans (le_mul_of_one_le_left h1.le h2)
· simp_all
· simpa only [← abs_mul, A_c_eq_zero h10] using (le_mul_iff_one_le_left h1).mpr h2
