toLinOfInv — Mathlib

English

Let M,M' be inverse matrices as above. For x ∈ M1 and any scalar m1 ∈ R, the action of the inverse matrix on m1 x matches the scalar action: (toLin v2 v1 M') (m1 x) = m1 ((toLin v1 v2 M) x).

Русский

Пусть M,M' обратны. Для x ∈ M1 и любого скаляра m1 ∈ R выполняется: (toLin v2 v1 M')(m1 x) = m1 ((toLin v1 v2 M) x).

LaTeX

$$$\mathrm{toLin}_{v_2,v_1}(M')(m_1 x) = m_1 \cdot \mathrm{toLin}_{v_1,v_2}(M)(x)$$$

Lean4

/-- If `M` and `M` are each other's inverse matrices, `Matrix.toLin M` and `Matrix.toLin M'`
form a linear equivalence. -/
@[simps]
def toLinOfInv [DecidableEq m] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1) (hM'M : M' * M = 1) :
    M₁ ≃ₗ[R] M₂ :=
  { Matrix.toLin v₁ v₂ M with
    toFun := Matrix.toLin v₁ v₂ M
    invFun := Matrix.toLin v₂ v₁ M'
    left_inv := fun x ↦ by rw [← Matrix.toLin_mul_apply, hM'M, Matrix.toLin_one, id_apply]
    right_inv := fun x ↦ by rw [← Matrix.toLin_mul_apply, hMM', Matrix.toLin_one, id_apply] }

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