toLin'OfInv — Mathlib

English

If M and M' are mutual inverses, they yield a linear equivalence between coordinate representations of functions with respect to M and M'.

Русский

Если M и M' взаимно обратны, они задают линейное эквивалентство между координатными представлениями функций относительно M и M'.

LaTeX

$$$ \\text{If } M M' = I_n \\text{ and } M' M = I_m, \\text{ then } (m \\to R) \\cong (n \\to R) \\text{ via } \\mathrm{toLin'}(M'). $$$

Lean4

/-- If `M` and `M'` are each other's inverse matrices, they provide an equivalence between `m → A`
and `n → A` corresponding to `M.mulVec` and `M'.mulVec`. -/
@[simps]
def toLin'OfInv [Fintype m] [DecidableEq m] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1)
    (hM'M : M' * M = 1) : (m → R) ≃ₗ[R] n → R :=
  { Matrix.toLin' M' with
    toFun := Matrix.toLin' M'
    invFun := Matrix.toLin' M
    left_inv := fun x ↦ by rw [← Matrix.toLin'_mul_apply, hMM', Matrix.toLin'_one, id_apply]
    right_inv := fun x ↦ by rw [← Matrix.toLin'_mul_apply, hM'M, Matrix.toLin'_one, id_apply] }

Похожие утверждения