mathlib

ee5e5e82 - feat(algebra/ring/equiv): Add `ring_equiv.comp_symm` (#17045)

feat(algebra/ring/equiv): Add `ring_equiv.comp_symm` (#17045) Some lemmata needed for the study of inertia group. These lemmas already exist for `alg_equiv` under the corresponding names.