English
The product M * auxMat M k is block triangular with respect to the block partition that isolates the k-th index, allowing determinant factorization along blocks.
Русский
Произведение M * auxMat M k блочно-верхнетреугольно относительно разбиения на блоки, что позволяет факторизацию детерминанта по блокам.
LaTeX
$$$ (M * \\mathrm{auxMat} \\ M \\ k).BlockTriangular (\\cdot = k) $$$
Lean4
/-- `M * aux M k` is upper triangular. -/
theorem mul_auxMat_blockTriangular : (M * auxMat M k).BlockTriangular (· = k) := fun i j lt ↦
by
simp_rw [lt_iff_not_ge, le_Prop_eq, Classical.not_imp] at lt
simp_rw [Matrix.mul_apply, auxMat, of_apply, if_neg lt.2, mul_ite, mul_neg, mul_zero]
rw [Finset.sum_ite, Finset.filter_eq', if_pos (Finset.mem_univ _), Finset.sum_singleton, Finset.sum_ite_eq', if_pos,
lt.1, mul_comm, neg_add_cancel]
exact Finset.mem_filter.mpr ⟨Finset.mem_univ _, lt.2⟩
