Zulip Chat Archive

Stream: new members

Topic: Vector space isomorphism


view this post on Zulip Nicolò Cavalleri (Jul 02 2020 at 14:33):

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

view this post on Zulip Eric Wieser (Jul 02 2020 at 14:33):

Possibly equiv, but I'm no expert

view this post on Zulip Mario Carneiro (Jul 02 2020 at 14:35):

there is a src#linear_equiv type I believe

view this post on Zulip Nicolò Cavalleri (Jul 02 2020 at 14:42):

Mario Carneiro said:

there is a src#linear_equiv type I believe

Ok thanks!

view this post on Zulip Kevin Buzzard (Jul 02 2020 at 14:44):

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.

view this post on Zulip Bryan Gin-ge Chen (Jul 02 2020 at 15:35):

@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).


Last updated: May 11 2021 at 13:22 UTC