English
If M and M' are mutual inverses, they induce a linear equivalence between the right-acting spaces, given by right multiplication by M and M'.
Русский
Если M и M' взаимно обратны, они порождают линейное эквивалентство между правыми пространствами, действующими справа умножением на M и M'.
LaTeX
$$toLinearEquivRight'OfInv hMM' hM'M : (n → R) ≃ₗ[R] (m → R)$$
Lean4
/-- Linear maps `(m → R) →ₗ[R] (n → R)` are linearly equivalent over `Rᵐᵒᵖ` to `Matrix m n R`,
by having matrices act by right multiplication.
-/
def toMatrixRight' : ((m → R) →ₗ[R] n → R) ≃ₗ[Rᵐᵒᵖ] Matrix m n R
where
toFun f i j := f (single R (fun _ ↦ R) i 1) j
invFun := Matrix.vecMulLinear
right_inv
M := by
ext i j
simp
left_inv
f := by
apply (Pi.basisFun R m).ext
intro j; ext i
simp
map_add' f
g := by
ext i j
simp only [Pi.add_apply, LinearMap.add_apply, Matrix.add_apply]
map_smul' c
f := by
ext i j
simp only [Pi.smul_apply, LinearMap.smul_apply, RingHom.id_apply, Matrix.smul_apply]
