Commit 2025-07-14 05:43 1b078c8d

View on Github →

chore(Algebra/Equiv/TransferInstance): split according to algebraic structures (#26732) Split Algebra.Equiv.TransferInstance into

  • Algebra.Group.TransferInstance
  • Algebra.GroupWithZero.TransferInstance
  • Algebra.Ring.TransferInstance
  • Algebra.Field.TransferInstance
  • Algebra.Module.TransferInstance
  • Algebra.Algebra.TransferInstance Restore the Nontrivial (Shrink α) instance that was accidentally deleted in #26774.

Estimated changes

added def Equiv.algEquiv
added theorem Equiv.algEquiv_apply
added theorem Equiv.algebraMap_def
deleted def Equiv.algEquiv
deleted theorem Equiv.algEquiv_apply
deleted theorem Equiv.algEquiv_symm_apply
deleted theorem Equiv.algebraMap_def
deleted def Equiv.linearEquiv
deleted def Equiv.ringEquiv
deleted theorem Equiv.ringEquiv_apply
deleted theorem LinearEquiv.isScalarTower
added def Equiv.ringEquiv
added theorem Equiv.ringEquiv_apply