Commit 2026-02-10 19:29 32a03d8c
View on Github →feat: {Continuous}Linear{Isometry}Equiv.conj{Continuous, Star}AlgEquiv are "almost" injective (#33417)
... "almost" meaning that they are colinear. I.e., f.conj{Continuous, Star}AlgEquiv S = g.conj{Continuous, Star}AlgEquiv S iff f = α • g for some unit(ary) α.
Also, the same for Unitary.conjStarAlgAut. All in one PR since they all have analogous proofs.