Zulip Chat Archive

Stream: new members

Topic: Declare column vector in Lean


view this post on Zulip 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 α)

view this post on Zulip 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) α.

view this post on Zulip Simon Hudon (Mar 15 2019 at 03:54):

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

view this post on Zulip Nguyen Thi Nhung (Mar 15 2019 at 04:39):

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

view this post on Zulip 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  α

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Nguyen Thi Nhung (Mar 19 2019 at 07:39):

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

view this post on Zulip 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