Zulip Chat Archive

Stream: new members

Topic: import fails


Chris M (Aug 22 2020 at 06:30):

I'm trying to use permutation perm, for which I'm trying to import data:

import algebra
import data

theorem cayley (G:Type*) [h:group G] :  f: G  perm G,

But Lean gives me this error under import algebra:

file 'data' not found in the search path
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more

and this one under import data:

invalid import: data
could not resolve import: data

Alex J. Best (Aug 22 2020 at 06:34):

You want import data.equiv, and likewise for algebra a filename after the .

Alex J. Best (Aug 22 2020 at 06:36):

Probably  algebra.group.basic

Chris M (Aug 22 2020 at 07:30):

This is what I have now:

import algebra
import data.equiv
import group_theory.group_action
import algebra.group.hom

theorem cayley (G:Type*) [h:group G] :  f: G →* perm G, f=f := sorry

But this gives the same error as before, now regarding data.equiv instead.

It works if I remove import data.equiv and instead write theorem cayley (G:Type*) [h:group G] : ∃ f: G →* equiv.perm G, f=f := sorry, but I don't wanna write equiv.perm all the time.

Scott Morrison (Aug 22 2020 at 08:09):

I think you are confused about import and open.

Scott Morrison (Aug 22 2020 at 08:09):

import is for importing the content of files, but have no bearing on namespaces or how you refer to identifiers.

Scott Morrison (Aug 22 2020 at 08:10):

open opens namespaces, so you can omit prefixes of fully qualified names.

Kyle Miller (Aug 22 2020 at 08:22):

Something you might consider doing is to define a homomorphism rather than proving existence:

def cayley (G : Type*) [h : group G] : G →* perm G := sorry

This is stronger because then proofs about cayley can make use of how it was defined. And, the fact you defined it means it exists.

Alex Zhang (Jul 13 2021 at 09:56):

I am editing the file \src\data\matrix\basic.lean and I added a new import import data.complex.basic
but why does the code then report

invalid import: data.complex.basic
could not resolve import: data.complex.basic

after a long time of "loading..."?

Anne Baanen (Jul 13 2021 at 09:56):

It is quite possible that data.complex.basic imports data.matrix.basic transitively.

Eric Wieser (Jul 13 2021 at 09:57):

At any rate I don't think data.matrix.basic should be importing the complex numbers

Eric Wieser (Jul 13 2021 at 09:58):

I assume you're wanting to define the conjugate transpose?

Alex Zhang (Jul 13 2021 at 09:58):

Yes, indeed.

Eric Wieser (Jul 13 2021 at 09:59):

If so, you don't need the complex numbers, you can define it on matrices over any star_ring

Alex Zhang (Jul 13 2021 at 10:00):

good suggestion!

Anne Baanen (Jul 13 2021 at 10:01):

data/matrix/basic.lean is also quite long, so could you define it in a new file?

Alex Zhang (Jul 13 2021 at 10:03):

transpose is defined in that file. I am considering defining conj_trans close to that. Would that be ok?

Eric Wieser (Jul 13 2021 at 10:05):

Probably the easiest way to shrink matrix/basic is to put all the block matrix stuff in a new file

Alex Zhang (Jul 13 2021 at 10:07):

I think I am going to add conj_trans close to transpose as it seems inconvenient for the users to me to put these two in different files.

Eric Wieser (Jul 13 2021 at 10:07):

I think conj_trans fits nicely in basic, probably right before the star_ring instance

Alex Zhang (Jul 13 2021 at 10:08):

Good suggestion! I think I am going to do this work first. Perhaps someone else can put out things that should be in a new file.

Eric Wieser (Jul 13 2021 at 10:09):

Thoughts on conj_transpose vs conj_trans?

Alex Zhang (Jul 13 2021 at 10:09):

I prefer conj_transpose

Eric Wieser (Jul 13 2021 at 10:09):

Do you have a notation in mind?

Alex Zhang (Jul 13 2021 at 10:11):

I will do localized "postfix :1500 := matrix.conj_transpose" in matrix

Alex Zhang (Jul 13 2021 at 10:11):

as localized "postfix :1500 := matrix.transpose" in matrix has been in the file.

Eric Rodriguez (Jul 13 2021 at 10:48):

fwiw, you can put backticks in codeblocks by just surrounding it with more backticks:

I will do localized "postfix `ᴴ`:1500 := matrix.conj_transpose" in matrix

Eric Rodriguez (Jul 13 2021 at 10:49):

```````````````````````` is an example of a zillion backticks that works

Alex Zhang (Jul 13 2021 at 10:55):

I have finished adding it. I am making a PR.

Eric Wieser (Jul 13 2021 at 11:10):

The PR is #8289. IMO there's way too much going on in that, and it should be split into smaller PRs


Last updated: Dec 20 2023 at 11:08 UTC