mathlib3

40cc79df - feat(data/matrix/kronecker): lemmas about trace, det, and inv (#18610)

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