# Zulip Chat Archive

## Stream: new members

### Topic: Declare column vector in Lean

#### Nguyen Thi Nhung (Mar 15 2019 at 03:40):

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 (Mar 15 2019 at 03:54):

`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 (Mar 15 2019 at 03:54):

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

#### Nguyen Thi Nhung (Mar 15 2019 at 04:39):

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

#### Nguyen Thi Nhung (Mar 18 2019 at 04:38):

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 (Mar 18 2019 at 05:22):

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 (Mar 18 2019 at 05:22):

(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 (Mar 18 2019 at 08:00):

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 (Mar 18 2019 at 08:29):

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 (Mar 19 2019 at 07:39):

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

#### Nguyen Thi Nhung (Mar 19 2019 at 08:25):

@Scott Morrison I have already fixed it :-)

Last updated: May 17 2021 at 21:12 UTC