Commit 2025-07-11 19:04 73303bb6

View on Github →

chore(Algebra/Equiv/TransferInstance): delete duplicated Shrink material (#26774) Split Algebra.Small.Group into

  • Algebra.Group.Shrink
  • Algebra.GroupWithZero.Shrink Split Algebra.Small.Ring into
  • Algebra.Ring.Shrink
  • Algebra.Field.Shrink Split Algebra.Small.Module into
  • Algebra.Module.Shrink
  • Algebra.Algebra.Shrink Almost all of this duplicated the material in Algebra.Equiv.TransferInstance, which we therefore remove. This is the second part of #26732, split off for Eric's convenience.

Estimated changes

added def Shrink.algEquiv
added def algEquivShrink
added def Shrink.mulEquiv
modified theorem equivShrink_div
modified theorem equivShrink_inv
modified theorem equivShrink_mul
modified theorem equivShrink_smul
modified theorem equivShrink_symm_div
modified theorem equivShrink_symm_inv
modified theorem equivShrink_symm_mul
modified theorem equivShrink_symm_one
modified theorem equivShrink_symm_smul
deleted def algEquivShrink
added def Shrink.ringEquiv