mathlib documentation


Matrices of dual numbers are isomorphic to dual numbers over matrices #

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

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