Bundle these matrix operations: - [`Matrix.map`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/Defs.html#Matrix.map) - [`Matrix.submatrix`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/Defs.html#Matrix.submatrix) - [`Equiv.Perm.permMatrix`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/Permutation.html#Equiv.Perm.permMatrix) as various homomorphisms, such as: - `OneHom` - `ZeroHom` - `AddHom` - `AddMonoidHom` (already exists for `Matrix.map`: [`AddMonoidHom.mapMatrix`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Basic.html#AddMonoidHom.mapMatrix)) - `LinearMap` (already exists for `Matrix.map`: [`LinearMap.mapMatrix`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Basic.html#LinearMap.mapMatrix)) - `MonoidHom` - `MonoidWithZeroHom` - `RingHom` (already exists for `Matrix.map`: [`RingHom.mapMatrix`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Basic.html#RingHom.mapMatrix)) - `AlgHom` (already exists for `Matrix.map`: [`AlgHom.mapMatrix`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Basic.html#AlgHom.mapMatrix)) - `MulHom` - `NonUnitalRingHom` - `NonUnitalAlgHom` (whichever make sense)
Bundle these matrix operations:
Matrix.mapMatrix.submatrixEquiv.Perm.permMatrixas various homomorphisms, such as:
OneHomZeroHomAddHomAddMonoidHom(already exists forMatrix.map:AddMonoidHom.mapMatrix)LinearMap(already exists forMatrix.map:LinearMap.mapMatrix)MonoidHomMonoidWithZeroHomRingHom(already exists forMatrix.map:RingHom.mapMatrix)AlgHom(already exists forMatrix.map:AlgHom.mapMatrix)MulHomNonUnitalRingHomNonUnitalAlgHom(whichever make sense)