English
The inverse of a Kronecker product satisfies (A ⊗ B)^{-1} = A^{-1} ⊗ B^{-1}, with appropriate unit assumptions on det(A) and det(B).
Русский
Обратная Кронекера удовлетворяет (A ⊗ B)^{-1} = A^{-1} ⊗ B^{-1}, при соответствующих предположениях на детерминанты.
LaTeX
$$(A ⊗ B)^{-1} = A^{-1} ⊗ B^{-1}$$
Lean4
theorem inv_kronecker [Fintype m] [DecidableEq m] (A : Matrix m m α) (B : Matrix n n α) : (A ⊗ₖ B)⁻¹ = A⁻¹ ⊗ₖ B⁻¹ := by
-- handle the special cases where either matrix is not invertible
by_cases hA : IsUnit A.det
swap
· cases isEmpty_or_nonempty n
· subsingleton
have hAB : ¬IsUnit (A ⊗ₖ B).det := by
refine mt (fun hAB => ?_) hA
rw [det_kronecker] at hAB
exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_left hAB)
rw [nonsing_inv_apply_not_isUnit _ hA, zero_kronecker, nonsing_inv_apply_not_isUnit _ hAB]
by_cases hB : IsUnit B.det; swap
· cases isEmpty_or_nonempty m
· subsingleton
have hAB : ¬IsUnit (A ⊗ₖ B).det := by
refine mt (fun hAB => ?_) hB
rw [det_kronecker] at hAB
exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_right hAB)
rw [nonsing_inv_apply_not_isUnit _ hB, kronecker_zero, nonsing_inv_apply_not_isUnit _ hAB]
-- otherwise follows trivially from `mul_kronecker_mul`
· apply inv_eq_right_inv
rw [← mul_kronecker_mul, ← one_kronecker_one, mul_nonsing_inv _ hA, mul_nonsing_inv _ hB]
