mul — Mathlib

English

The transvection i j c is block triangular with respect to b when b i ≤ b j (standard variant).

Русский

Транспекция i j c блочно-треугольна по b, если b i ≤ b j (стандартный вариант).

LaTeX

$$$\BlockTriangular\bigl(\mathrm{transvection}\; i\; j\; c\bigr)\; b$ при $b i ≤ b j$$$

Lean4

theorem mul [Fintype m] [NonUnitalNonAssocSemiring R] {M N : Matrix m m R} (hM : BlockTriangular M b)
    (hN : BlockTriangular N b) : BlockTriangular (M * N) b :=
  by
  intro i j hij
  apply Finset.sum_eq_zero
  intro k _
  by_cases hki : b k < b i
  · simp_rw [hM hki, zero_mul]
  · simp_rw [hN (lt_of_lt_of_le hij (le_of_not_gt hki)), mul_zero]

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