Commit 2023-03-19 20:21 40cc79df

feat(data/matrix/kronecker): lemmas about trace, det, and inv (#18610) The key results here are:

• det (A ⊗ₖ B) = det A ^ fintype.card n * det B ^ fintype.card m
• trace (A ⊗ₖ B) = trace A * trace B
• (A ⊗ₖ B)⁻¹ = (A⁻¹ ⊗ₖ B⁻¹) and the tensor analogues:
• det (A ⊗ₖₜ[R] B) = (det A ^ fintype.card n) ⊗ₜ[R] (det B ^ fintype.card m)
• trace (A ⊗ₖₜ[R] B) = trace A ⊗ₜ[R] trace B This also adds some lemmas linking the kronecker product to block diagonal matrices. Generalized from https://github.com/eric-wieser/lean-matrix-cookbook