mul_auxMat_corner — Mathlib

English

The lower-right corner of M * auxMat M k equals the corresponding corner of M, showing stability of that entry under the auxiliary transformation.

Русский

Нижний правый угол произведения M * auxMat M k равен соответствующему углу M, показывая устойчивость этого элемента при вспомогательном преобразовании.

LaTeX

$$$ (M * \\mathrm{auxMat} \\, M \\, k)_{k k} = M_{k k} $$$

Lean4

/-- The lower-right corner of `M * aux M k` is the same as the corner of `M`. -/
theorem mul_auxMat_corner : (M * auxMat M k) k k = M k k := by simp [Matrix.mul_apply, auxMat]

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