listTransvecCol_mul_last_col — Mathlib

English

If the last entry of the last row of M is nonzero, then multiplying on the left by the product of all transvections in listTransvecCol M kills all the entries in the last column except possibly the bottom-right entry; in particular, for i in Fin r, (listTransvecCol M).prod * M has zero in the (inl i, inr unit) position.

Русский

Если последнее значение в последнем столбце матрицы M ненулевое, то произведение всех транспектаций слева из списка listTransvecCol M обнуляет все остальные элементы в последнем столбце, оставляя лишь возможно не нулевой элемент в нижнем правом углу.

LaTeX

$$$\forall hM: M(inr\,unit, inr\,unit) \neq 0,\; \forall i: Fin\,r,\; ((listTransvecCol\,M).prod * M)(inl\,i)(inr\,unit) = 0$$$

Lean4

/-- Multiplying by all the matrices in `listTransvecCol M` kills all the coefficients in the
last column but the last one. -/
theorem listTransvecCol_mul_last_col (hM : M (inr unit) (inr unit) ≠ 0) (i : Fin r) :
    ((listTransvecCol M).prod * M) (inl i) (inr unit) = 0 :=
  by
  suffices H :
    ∀ k : ℕ,
      k ≤ r → (((listTransvecCol M).drop k).prod * M) (inl i) (inr unit) = if k ≤ i then 0 else M (inl i) (inr unit)
    by simpa only [List.drop, _root_.zero_le, ite_true] using H 0 (zero_le _)
  intro k hk
  induction hk using Nat.decreasingInduction with
  | of_succ n hn IH =>
    have hn' : n < (listTransvecCol M).length := by simpa [listTransvecCol] using hn
    let n' : Fin r := ⟨n, hn⟩
    rw [List.drop_eq_getElem_cons hn']
    have A :
      (listTransvecCol M)[n] = transvection (inl n') (inr unit) (-M (inl n') (inr unit) / M (inr unit) (inr unit)) := by
      simp [n', listTransvecCol]
    simp only [Matrix.mul_assoc, A, List.prod_cons]
    by_cases h : n' = i
    · have hni : n = i := by
        cases i
        simp only [n', Fin.mk_eq_mk] at h
        simp [h]
      simp only [h, transvection_mul_apply_same, IH, ← hni, add_le_iff_nonpos_right,
        listTransvecCol_mul_last_row_drop _ _ hn]
      simp [field]
    · have hni : n ≠ i := by
        rintro rfl
        cases i
        simp [n'] at h
      simp only [ne_eq, inl.injEq, Ne.symm h, not_false_eq_true, transvection_mul_apply_of_ne]
      rw [IH]
      rcases le_or_gt (n + 1) i with (hi | hi)
      · simp only [hi, n.le_succ.trans hi, if_true]
      · rw [if_neg, if_neg]
        · simpa only [hni.symm, not_le, or_false] using Nat.lt_succ_iff_lt_or_eq.1 hi
        · simpa only [not_le] using hi
  | self =>
    simp only [length_listTransvecCol, le_refl, List.drop_eq_nil_of_le, List.prod_nil, Matrix.one_mul]
    rw [if_neg]
    simpa only [not_le] using i.2

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