Zulip Chat Archive

Stream: Is there code for X?

Topic: Cauchy Binet theorem

Yufei Liu (Sep 23 2023 at 07:57):

Has Cauchy Binet theorem been formalised in LEAN? how close are we?

Kevin Buzzard (Sep 23 2023 at 11:01):

guessing docs#Matrix.det_mul

Kevin Buzzard (Sep 23 2023 at 11:02):

Oh -- this is not the theorem, so maybe not?

Kevin Buzzard (Sep 23 2023 at 11:04):

I guess even formalising the statement will be an interesting exercise.

Yufei Liu (Sep 25 2023 at 13:58):

Kevin Buzzard said:

I guess even formalising the statement will be an interesting exercise.

I see, thank you for your reply!

Last updated: Dec 20 2023 at 11:08 UTC