Commit 2026-02-25 05:21 c73c4744
View on Github →refactor(Algebra/*): generalize of_ringEquiv lemmas (#35351)
Some lemmas assumed that two modules over different rings
admit a semilinear equivalence with respect to a RingEquiv.
While this is mathematically equivalent
to the definition we use everywhere else
(a pair of RingHoms with RingHomInvPair assumptions),
it does not directly apply neither to the linear case,
nor to the starRingEnd case.
This PR drops of_ringEquiv theorems
and generalizes of_equiv theorems
to semilinear equivalences instead.