Commit 2023-10-09 10:41 28df819d
View on Github →refactor(Algebra/Algebra/Equiv): align AlgEquiv.ofLinearEquiv with AlgHom.ofLinearMap (#7537)
The former previously took a hypothesis about f (algebraMap R A r) = algebraMap R B r, but now needs only f 1 = 1, matching the latter. This doesn't make much difference at the two callers.