Matrices of dual numbers are isomorphic to dual numbers over matrices

Showing this for the more general case of TrivSqZeroExt R M would require an action between Matrix n n R and Matrix n n M, which would risk causing diamonds.

@[simp]

theorem Matrix.dualNumberEquiv_symm_apply {R : Type} {n : Type} [CommSemiring R] [Fintype n] [DecidableEq n] (d : DualNumber (Matrix n n R)) : ↑(AlgEquiv.symm Matrix.dualNumberEquiv) d = ↑Matrix.of fun i j => (TrivSqZeroExt.fst (Matrix n n R) (Matrix n n R) d i j, TrivSqZeroExt.snd (Matrix n n R) (Matrix n n R) d i j)

@[simp]

theorem Matrix.dualNumberEquiv_apply {R : Type} {n : Type} [CommSemiring R] [Fintype n] [DecidableEq n] (A : Matrix n n (DualNumber R)) : ↑Matrix.dualNumberEquiv A = (↑Matrix.of fun i j => TrivSqZeroExt.fst (A i j), ↑Matrix.of fun i j => TrivSqZeroExt.snd (A i j))

def Matrix.dualNumberEquiv {R : Type} {n : Type} [CommSemiring R] [Fintype n] [DecidableEq n] : Matrix n n (DualNumber R) ≃ₐ[R] DualNumber (Matrix n n R)

Matrices over dual numbers and dual numbers over matrices are isomorphic.