Vector space isomorphism

Stream: new members

[Nicolò Cavalleri]

I was wondering how do you express that two modules or two vector spaces are isomorphic. I see that there is a structure for linear map but I do not find any for isomorphism

[Eric Wieser]

Possibly equiv, but I'm no expert

[Mario Carneiro]

there is a src#linear_equiv type I believe

[Nicolò Cavalleri]

Mario Carneiro said:

there is a src#linear_equiv type I believe

Ok thanks!

[Kevin Buzzard]

Weirdly I was looking at that definition about an hour ago, because I edited linear_algebra.basic in a PR and the linter complained; it turned out that the issue is that linear_equiv.to_equiv and some other similar defs hadn't got docstrings.

[Bryan Gin-ge Chen]

@Kevin Buzzard That sounds like #2409. I believe the solution is to either add @[nolint doc_blame] or to use add_decl_doc to add a docstring after the fact (e.g. here).