feat: port Data.Matrix.DualNumber (#3239)

Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib.lean

@@ -778,6 +778,7 @@ import Mathlib.Data.List.Zip
 import Mathlib.Data.ListM
 import Mathlib.Data.Matrix.Basic
 import Mathlib.Data.Matrix.DMatrix
+import Mathlib.Data.Matrix.DualNumber
 import Mathlib.Data.Matrix.Hadamard
 import Mathlib.Data.Multiset.Antidiagonal
 import Mathlib.Data.Multiset.Basic

Mathlib/Data/Matrix/DualNumber.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2023 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+
+! This file was ported from Lean 3 source module data.matrix.dual_number
+! leanprover-community/mathlib commit eb0cb4511aaef0da2462207b67358a0e1fe1e2ee
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Algebra.DualNumber
+import Mathlib.Data.Matrix.Basic
+
+/-!
+# 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.
+-/
+
+
+variable {R n : Type} [CommSemiring R] [Fintype n] [DecidableEq n]
+
+open Matrix TrivSqZeroExt
+
+/-- Matrices over dual numbers and dual numbers over matrices are isomorphic. -/
+@[simps]
+def Matrix.dualNumberEquiv : Matrix n n (DualNumber R) ≃ₐ[R] DualNumber (Matrix n n R) where
+  toFun A := ⟨of fun i j => (A i j).fst, of fun i j => (A i j).snd⟩
+  invFun d := of fun i j => (d.fst i j, d.snd i j)
+  left_inv A := Matrix.ext fun i j => TrivSqZeroExt.ext rfl rfl
+  right_inv d := TrivSqZeroExt.ext (Matrix.ext fun i j => rfl) (Matrix.ext fun i j => rfl)
+  map_mul' A B := by
+    ext; dsimp [mul_apply]
+    · simp_rw [fst_sum, fst_mul]
+      rfl
+    · simp_rw [snd_sum, snd_mul, smul_eq_mul, op_smul_eq_mul, Finset.sum_add_distrib]
+      simp [mul_apply, snd_sum, snd_mul]
+      rw [← Finset.sum_add_distrib]
+  map_add' A B := TrivSqZeroExt.ext rfl rfl
+  commutes' r := by
+    simp_rw [algebraMap_eq_inl', algebraMap_eq_diagonal, Pi.algebraMap_def,
+      Algebra.id.map_eq_self, algebraMap_eq_inl, ← diagonal_map (inl_zero R), map_apply, fst_inl,
+      snd_inl]
+    rfl
+#align matrix.dual_number_equiv Matrix.dualNumberEquiv