Declare column vector in Lean

Stream: new members

[Nguyen Thi Nhung]

Hello, I am trying to formalize Cramer rule in Lean. I need to declare a column vector. I did as the following, but it had errors. Anyone can help me? Thanks alot.

import ring_theory.determinant
open matrix
universes u v
variables (n : Type u) [fintype n][decidable_eq n]
variables (α : Type v)[field α]
variables [has_one (Type u)](A: matrix n n α)(b: matrix n 1 α)

[Simon Hudon]

n should probably be a nat, not a type. Then I'd use matrix (fin n) (fin n) α and matrix (fin n) (fin 1) α.

[Simon Hudon]

For future reference you should include the error messages in with your question

[Nguyen Thi Nhung]

@Simon Hudon. Following your suggestions, I did it. Thank you.

[Nguyen Thi Nhung]

Hi,
I am formalizing Cramer rule, but it still has error (as I include in the following). How can I solve it? Thank you.

import ring_theory.determinant algebra.field
open matrix
open units

universe v
variables (n:ℕ)(α : Type v)[field α]

theorem Cramer_rule{A: matrix (fin n)(fin n) α }{x : matrix (fin n) (fin 1) α}{b : matrix (fin n) (fin 1) α}
(h1: A.mul x = b)(h2: det(A) ≠ 0) : x = (λ t, det(λ i j, if j = t then b i 1 else A i j)/ det(A)) := sorry

type mismatch at application
  ite (j = t) (b i 1)
term
  b i 1
has type
  α
but is expected to have type
  fin 1 → α

[Scott Morrison]

Do you understand what the error message is saying? The point is that x is an n-by-1 matrix, but in your conclusion you are saying x = ?, for ? just a vector.

[Scott Morrison]

(i.e. just a function from fin n to alpha, rather than a function from fin n to fin 1 to alpha.)

[Nguyen Thi Nhung]

Thank you for your reply @Scott Morrison . I knew my error, but I didn't know how to solve it :slight_smile: . Can you show me how to correct this?

[Scott Morrison]

Well, your expression λ t, det(λ i j, if j = t then b i 1 else A i j)/ det(A)) is a function fin n -> \alpha, and you need a fin n -> fin 1 -> \alpha. What is the the syntax you might use to define a function of two arguments?

[Nguyen Thi Nhung]

@Scott Morrison Thank you. I will think about this to fix my error.

[Nguyen Thi Nhung]

@Scott Morrison I have already fixed it :-)