English
If M is a matrix and p,q are predicates on m with q x ↔ p x, then the determinants of the corresponding block-structured matrices are equal.
Русский
Если M — матрица, и p,q — предикаты на m с условием q x ↔ p x, то детерминанты соответствующих блочно-структурированных матриц равны.
LaTeX
$$$(\text{toSquareBlockProp } M\, p).det = (\text{toSquareBlockProp } M\, q).det$ при $\forall x, q x \iff p x$$$
Lean4
theorem equiv_block_det (M : Matrix m m R) {p q : m → Prop} [DecidablePred p] [DecidablePred q] (e : ∀ x, q x ↔ p x) :
(toSquareBlockProp M p).det = (toSquareBlockProp M q).det := by
convert
Matrix.det_reindex_self (Equiv.subtypeEquivRight e)
(toSquareBlockProp M q)
-- Removed `@[simp]` attribute,
-- as the LHS simplifies already to `M.toSquareBlock id i ⟨i, ⋯⟩ ⟨i, ⋯⟩`
