Zulip Chat Archive
Stream: general
Topic: Finite dimensional linear algebra
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?
Kenny Lau (Jul 05 2018 at 15:43):
did I?
Kenny Lau (Jul 05 2018 at 15:43):
@Kevin Buzzard it might be the one from year 2
Chris Hughes (Jul 05 2018 at 15:45):
Authors: Johannes Hölzl, Kenny Lau from the top of linear_algebra.linear_map_module
Kenny Lau (Jul 05 2018 at 15:45):
but those are in mathlib
Blair Shi (Jul 05 2018 at 15:48):
I found them.
Kevin Buzzard (Jul 05 2018 at 17:14):
Is it worth making a new type finite_dimensional_vector_space?
Blair Shi (Jul 06 2018 at 17:28):
Yup, I think we need to make a new type for it
Last updated: Dec 20 2023 at 11:08 UTC