## 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.

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: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