import fails

Stream: new members

[Chris M]

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]

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

[Alex J. Best]

Probably  algebra.group.basic

[Chris M]

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]

I think you are confused about import and open.

[Scott Morrison]

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

[Scott Morrison]

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

[Kyle Miller]

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]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Alex Zhang]

Yes, indeed.

[Eric Wieser]

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

[Alex Zhang]

good suggestion!

[Anne Baanen]

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

[Alex Zhang]

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

[Eric Wieser]

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

[Alex Zhang]

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]

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

[Alex Zhang]

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]

Thoughts on conj_transpose vs conj_trans?

[Alex Zhang]

I prefer conj_transpose

[Eric Wieser]

Do you have a notation in mind?

[Alex Zhang]

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

[Alex Zhang]

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

[Eric Rodriguez]

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]

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

[Alex Zhang]

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

[Eric Wieser]

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