English
The composition of mulLeftRight with its inverse equals the identity on End_Matrix; a formal cancellation property holds for the matrix case.
Русский
Композиция mulLeftRight и его обратной карты даёт тождество на End-матрицах; свойство аннулирования в матричном случае сохраняется.
LaTeX
$$$(\text{mulLeftRightMatrix_inv } R n) \circ (\text{mulLeftRight } R (\text{Matrix } n\, n\, R)).toLinearMap = \mathrm{id}$$$
Lean4
theorem inv_comp : (AlgHom.mulLeftRightMatrix_inv R n).comp (AlgHom.mulLeftRight R (Matrix n n R)).toLinearMap = .id :=
((Matrix.stdBasis _ _ _).tensorProduct ((Matrix.stdBasis _ _ _).map (opLinearEquiv ..))).ext fun ⟨⟨i0, j0⟩, k0, l0⟩ ↦
by simp [stdBasis_eq_single, ite_and, Fintype.sum_prod_type, mulLeftRight_apply, single, Matrix.mul_apply]
