Zulip Chat Archive

Stream: general

Topic: Finite dimensional linear algebra


view this post on Zulip Blair Shi (Jul 05 2018 at 15:42):

@Kenny Lau I am currently doing linear algebra on lean. I heard that you already did something on it. Could you plz tell me how far are you?

view this post on Zulip Kenny Lau (Jul 05 2018 at 15:43):

did I?

view this post on Zulip Kenny Lau (Jul 05 2018 at 15:43):

@Kevin Buzzard it might be the one from year 2

view this post on Zulip Chris Hughes (Jul 05 2018 at 15:45):

Authors: Johannes Hölzl, Kenny Lau from the top of linear_algebra.linear_map_module

view this post on Zulip Kenny Lau (Jul 05 2018 at 15:45):

but those are in mathlib

view this post on Zulip Blair Shi (Jul 05 2018 at 15:48):

I found them.

view this post on Zulip Kevin Buzzard (Jul 05 2018 at 17:14):

Is it worth making a new type finite_dimensional_vector_space?

view this post on Zulip Blair Shi (Jul 06 2018 at 17:28):

Yup, I think we need to make a new type for it


Last updated: May 14 2021 at 22:15 UTC