auxMat_toSquareBlock_eq — Mathlib

English

The lower-right square block of the auxiliary construction equals M k k • 1, reflecting a canonical corner value preserved in the augmentation.

Русский

Нижний правый квадратный блок вспомогательной конструкции равен M k k • 1, отражая сохранённое значение угла.

LaTeX

$$$ (\\mathrm{auxMat} \\, M \\, k).toSquareBlock (\\cdot \\neq k) False = M_{k k} \\cdot 1 $$$

Lean4

theorem auxMat_toSquareBlock_eq : (auxMat M k).toSquareBlock (· ≠ k) False = 1 :=
  by
  ext ⟨i, hi⟩ ⟨j, hj⟩
  rw [eq_iff_iff, iff_false, not_not] at hi hj
  simp [auxMat, toSquareBlock_def, if_pos hi, if_pos hj, Matrix.one_apply, if_pos (hj ▸ hi)]

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