Commit 2025-01-07 04:59 57f8888c
View on Github →chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version (#20416)
Move the two definitions MonoidHom.precompEquiv (the equivalence (β →* γ) ≃ (α →* γ) obtained by precomposition with a multiplicative equivalence e : α ≃* β) and AddMonoidHom.precompEquiv (its additive version) from Algebra.Category.MonCat.ForgetCorepresentable to Algebra.Group.Equiv.Basic, so they can be used without importing files about MonCat. Also merge them into one definition using @[to_additive] and add the symmetric definition (Add)MonoidHom.postcompEquiv.