Zulip Chat Archive
Stream: mathlib4
Topic: Module automorphisms
Calle Sönne (Sep 02 2024 at 18:52):
Is there a definition of the type of automorphisms of a module, similar to Module.End? If it does not exist, is there a reason for this (i.e. should I access this type in another way)?
Eric Wieser (Sep 02 2024 at 19:02):
Calle Sönne (Sep 02 2024 at 19:03):
Aha! Thank you :)
Oliver Nash (Sep 03 2024 at 20:33):
Also docs#LinearEquiv
Matthew Ballard (Sep 03 2024 at 20:35):
I am not sure I have ever used this terminology outside Spec R points of GL.
Patrick Massot (Sep 04 2024 at 10:48):
Which terminology? General Linear? Isn’t it what GL stands for?
Last updated: May 02 2025 at 03:31 UTC