matrices

Stream: new members

[Alex Zhang]

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]

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]

Can you use something like is_unit_det_of_left_inverse?

[Alex Zhang]

Yes! I think I am going to add it.

[Alex Zhang]

The above is a reply to Kevin.

[Chris Birkbeck]

Or perhaps is_unit_iff_is_unit_det

[Kevin Buzzard]

Nice! Chris' suggestions should make this painless.

[Alex Zhang]

Cool!

[Alex Zhang]

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

[Chris Birkbeck]

I have some explict GLn stuff if you are interested.

[Alex Zhang]

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

[Alex Zhang]

Another important thing, is matrix similarity defined in matlib?

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

The difference is not mathematical, of course.

[Johan Commelin]

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

[Alex Zhang]

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]

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]

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

[Alex Zhang]

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

[Yakov Pechersky]

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]

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