Matrix-vector multiplication with inverse matrices

Stream: new members

[Eric Demers]

I'm trying to prove that a 2×2 linear system with non-zero determinant has a unique solution. I want to use the matrix inverse approach but I'm stuck on connecting matrix inverses with mulVec.

Here's my attempt:

lean

import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic

variable {R : Type*} [Field R] [Fintype (Fin 2)] [DecidableEq (Fin 2)] in
lemma matrix_2x2_unique (A : Matrix (Fin 2) (Fin 2) R) (b : Fin 2 → R) (h : A.det ≠ 0) :
    ∃! x : Fin 2 → R, A *ᵥ x = b := by
  haveI : IsUnit A.det := IsUnit.mk0 _ h
  haveI : Invertible A := Matrix.invertibleOfIsUnitDet A this

  use A⁻¹ *ᵥ b
  constructor
  · -- Existence: need to show A *ᵥ (A⁻¹ *ᵥ b) = b
    -- How do I use that A * A⁻¹ = 1 with mulVec?
    sorry
  · -- Uniqueness: if A *ᵥ y = b, then y = A⁻¹ *ᵥ b
    intro y hy
    -- How do I show A⁻¹ *ᵥ (A *ᵥ y) = y?
    sorry

I know that A * A⁻¹ = 1 when A is invertible, but I can't find the right lemma to connect this with mulVec. Is there a lemma like (A * B) *ᵥ v = A *ᵥ (B *ᵥ v)? Or should I be using a different approach entirely?

[Aaron Liu]

you probably don't want [Fintype (Fin 2)] [DecidableEq (Fin 2)] in your variables

[Aaron Liu]

when I put your code into the web editor, I get error: expected token on line 6 col. 25, can you fix this error please (maybe missing an open namespace?)

[Ilmārs Cīrulis]

My try

import Mathlib

open Matrix

variable {R : Type*} [Field R] in
lemma matrix_2x2_unique (A : Matrix (Fin 2) (Fin 2) R) (b : Fin 2 → R) (h : A.det ≠ 0) :
    ∃! x : Fin 2 → R, A *ᵥ x = b := by
  haveI : IsUnit A.det := IsUnit.mk0 _ h
  haveI : Invertible A := Matrix.invertibleOfIsUnitDet A this

  use A⁻¹ *ᵥ b
  constructor
  · simp only
    rw [mulVec_mulVec, mul_inv_of_invertible, one_mulVec]
  · intro y hy
    rw [← hy, mulVec_mulVec, inv_mul_of_invertible, one_mulVec]

[Eric Demers]

Thank you so much! Really appreciate the help!