English
A second composition equality holds in the matrix setting, reinforcing the double-sided inverse property.
Русский
Вторая запись композиции сохраняет двойной обратный закон в матричном случае.
LaTeX
$$$(\mathrm{mulLeftRightMatrix_inv } R n) \circ (\mathrm{mulLeftRight } R (\mathrm{Matrix } n\, n\, R)).toLinearMap = \mathrm{id}$$$
Lean4
theorem comp_inv : (AlgHom.mulLeftRight R (Matrix n n R)).toLinearMap.comp (AlgHom.mulLeftRightMatrix_inv R n) = .id :=
by
ext f : 1
apply (Matrix.stdBasis _ _ _).ext
intro ⟨i, j⟩
simp only [LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply, map_sum, map_smul,
stdBasis_eq_single, LinearMap.coeFn_sum, Finset.sum_apply, LinearMap.smul_apply, LinearMap.id_coe, id_eq]
ext k l
simp [sum_apply, Matrix.mul_apply, single, Fintype.sum_prod_type, ite_and]
