Commit 2024-06-03 05:47 52b851a9

View on Github →

chore(Algebra–GroupTheory): remove refine' (#13472) Split from #13385; this excludes usages where refine' was used to replace refine_struct.

Estimated changes

modified theorem IsRingHom.id
modified theorem IsSemiringHom.id