Transfer algebraic structures across Equivs

This continues the pattern set in Mathlib/Algebra/Group/TransferInstance.lean.

@[reducible, inline]

abbrev Equiv.algebra (R : Type u_1) {α : Type u_2} {β : Type u_3} [CommSemiring R] (e : α ≃ β) [Semiring β] : have x := e.semiring; [Algebra R β] → Algebra R α

Transfer Algebra across an Equiv

theorem Equiv.algebraMap_def {R : Type u_1} {α : Type u_2} {β : Type u_3} [CommSemiring R] (e : α ≃ β) [Semiring β] [Algebra R β] (r : R) : (algebraMap R α) r = e.symm ((algebraMap R β) r)

def Equiv.algEquiv (R : Type u_1) {α : Type u_2} {β : Type u_3} [CommSemiring R] (e : α ≃ β) [Semiring β] [Algebra R β] : let semiring := e.semiring; have algebra := Equiv.algebra R e; α ≃ₐ[R] β

An equivalence e : α ≃ β gives an algebra equivalence α ≃ₐ[R] β where the R-algebra structure on α is the one obtained by transporting an R-algebra structure on β back along e.

@[simp]

theorem Equiv.algEquiv_apply {R : Type u_1} {α : Type u_2} {β : Type u_3} [CommSemiring R] (e : α ≃ β) [Semiring β] [Algebra R β] (a : α) : (algEquiv R e) a = e a

theorem Equiv.algEquiv_symm_apply {R : Type u_1} {α : Type u_2} {β : Type u_3} [CommSemiring R] (e : α ≃ β) [Semiring β] [Algebra R β] (b : β) : (AlgEquiv.symm (algEquiv R e)) b = e.symm b