English
A variant of the determinant identity: the product det(M) times M_{k k}^{(card m - 1)} equals M_{k k} times the determinant of a corresponding block, underpinning a key inductive step in norm calculations.
Русский
Вариант тождества детерминант: det(M) умноженное на M_{k k}^{(card m - 1)} равняется M_{k k} умноженному на детерминант соответствующего блока, поддерживая ключевой индуктивный шаг нормировки.
LaTeX
$$$ \\det(M) \\cdot M_{k k}^{(m-1)} = M_{k k} \\cdot \\det(\\mathrm{mulAuxMatBlock}).$$$
Lean4
theorem det_mul_corner_pow : M.det * M k k ^ (Fintype.card m - 1) = M k k * (mulAuxMatBlock).det :=
by
trans (M * auxMat M k).det
· simp [det_mul, (auxMat_blockTriangular M k).det_fintype, auxMat_toSquareBlock_ne, auxMat_toSquareBlock_eq]
rw [(mul_auxMat_blockTriangular M k).det_fintype, Fintype.prod_Prop, mul_auxMat_toSquareBlock_eq]
simp_rw [det_smul_of_tower, eq_iff_iff, iff_true, Fintype.card_unique, pow_one, det_one, smul_eq_mul, mul_one]
-- `Decidable (P = Q)` diamond induced by `Prop.linearOrder`, which is classical, when `P` and `Q`
-- are themselves decidable.
convert rfl
