Zulip Chat Archive

Stream: new members

Topic: matrices


Alex Zhang (Jun 30 2021 at 08:50):

variables {α I : Type*}
variables [decidable_eq I] [comm_ring α]
variables (A : matrix I I α) [invertible A]
example : is_unit A.det := by sorry

I think the following is a very basic fact in linear algebra. Is this proved in matlib? Lib search does not return a result.

Kevin Buzzard (Jun 30 2021 at 08:53):

If it's not then you could probably prove it by letting B be the inverse and showing det(A)det(B)=1. It is probably only a couple of lines. And if it's not there you could make a PR :-)

Chris Birkbeck (Jun 30 2021 at 08:53):

Can you use something like is_unit_det_of_left_inverse?

Alex Zhang (Jun 30 2021 at 08:53):

Yes! I think I am going to add it.

Alex Zhang (Jun 30 2021 at 08:54):

The above is a reply to Kevin.

Chris Birkbeck (Jun 30 2021 at 08:54):

Or perhaps is_unit_iff_is_unit_det

Kevin Buzzard (Jun 30 2021 at 08:55):

Nice! Chris' suggestions should make this painless.

Alex Zhang (Jun 30 2021 at 08:55):

Cool!

Alex Zhang (Jun 30 2021 at 08:58):

I am preparing a file about things relevant to some matrices operations. perhaps can add some stuff

Chris Birkbeck (Jun 30 2021 at 09:00):

I have some explict GLn stuff if you are interested.

Alex Zhang (Jun 30 2021 at 09:01):

Thanks! I will ask you for help if I need.

Alex Zhang (Jun 30 2021 at 09:02):

Another important thing, is matrix similarity defined in matlib?

Johan Commelin (Jun 30 2021 at 09:05):

@Alex Zhang I think in cases like this, it's better to write is_unit A instead of [invertible A].

Johan Commelin (Jun 30 2021 at 09:05):

See also https://leanprover-community.github.io/mathlib_docs/algebra/invertible.html for a (maybe a bit short) explanation.

Johan Commelin (Jun 30 2021 at 09:06):

[invertible x] is mostly intended for saying: I have a random ring, but please assume that 2 has an inverse.

Johan Commelin (Jun 30 2021 at 09:07):

For generic invertible elements, it's better to use either units R or is_unit r, for r : R

Johan Commelin (Jun 30 2021 at 09:07):

The difference is not mathematical, of course.

Johan Commelin (Jun 30 2021 at 09:07):

It has to do with type class inference, and other implementation details.

Alex Zhang (Jun 30 2021 at 09:22):

Thanks for your suggestion Johan, the built-in lemmas about matrix inverse use is_unit A.det.
is_unit A would be fine to me. is_unit A.det just seems a little bit tedious and indirect. I just want to build a little bridge between it and [invertible A].

Alex Zhang (Jun 30 2021 at 09:39):

The library research also does not return a result for this

variables [decidable_eq I] [comm_ring α]
variables (A : matrix I I α) (B : matrix J J α) (C : matrix I I α)

example (h : A  C = 1) : C = A⁻¹ := by library_search

Hasn't this been established? anything related?

Chris Birkbeck (Jun 30 2021 at 09:42):

Try having a look at the nonsingular_inverse.lean file. Its where I found most of these things.

Alex Zhang (Jun 30 2021 at 09:47):

It seems that I need to add a few more little bridges.

Yakov Pechersky (Jun 30 2021 at 13:21):

You might like to take a look at my formalization of an intro to group theory course. https://github.com/pechersky/e222/blob/master/src/lecture01.lean

Yakov Pechersky (Jun 30 2021 at 13:21):

That file shows a lot of the ways mathlib can be used to work with elementary results about GLn


Last updated: Dec 20 2023 at 11:08 UTC