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.

theorem Matrix.dualNumberEquiv_symm_apply {R : Type} {n : Type} [CommSemiring R] [Fintype n] [DecidableEq n] (d : DualNumber (Matrix n n R)) :
Matrix.dualNumberEquiv.symm d = Matrix.of fun (i j : n) => (TrivSqZeroExt.fst d i j, TrivSqZeroExt.snd d i j)
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 : n) => TrivSqZeroExt.fst (A i j), Matrix.of fun (i j : n) => TrivSqZeroExt.snd (A i j))

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

  • One or more equations did not get rendered due to their size.
Instances For