module.free ℝ (fin 2 → ℝ)

Stream: Is there code for X?

[Alex Kontorovich]

I would think this would be a simp lemma or something?... Thanks in advance!

import linear_algebra.free_module.basic
import data.real.basic

example : module.free ℝ (fin 2 → ℝ) := sorry

[Eric Wieser]

Does by apply_instance find it?

[Alex Kontorovich]

Nevermind, sorry. Librarysearch found it... (It was timing out before. So I moved it to the top of the file and used #exit...)

[Eric Wieser]

You shouldn't be using library_search for this anyway, it's a typeclass

[Eric Wieser]

Which means lean will just find it for you whever you need it

[Yakov Pechersky]

Why does docs#module.free say "Type ?" even though the source says it's the same universe as M?

[Eric Wieser]

Probably a bug in the doc-gen export

[Riccardo Brasca]

Note that if you also need that it is finite you may need to explicitly write

  letI : module.finite ℝ (fin 1.succ → ℝ) := module.finite.pi,

There is a discussion why sometimes Lean doesn't find it automatically, but I don't remember the details.

[Eric Wieser]

I just created #15956 to cleanup some mess around module.free

[Riccardo Brasca]

Thanks!