Theorem RingHomInvPair.of_ringEquiv_symm

Modification history

2026-02-25 05:21
Mathlib/Algebra/Ring/CompTypeclasses.lean
refactor(Algebra/*): generalize `of_ringEquiv` lemmas (#35351) …
Added RingHomInvPair.of_ringEquiv_symmView on Github →