Transfer algebraic structures across Equivs

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

def Equiv.ringEquiv {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Add β] [Mul β] : have add := e.add; have mul := e.mul; α ≃+* β

An equivalence e : α ≃ β gives a ring equivalence α ≃+* β where the ring structure on α is the one obtained by transporting a ring structure on β back along e.

@[simp]

theorem Equiv.ringEquiv_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Add β] [Mul β] (a : α) : e.ringEquiv a = e a

theorem Equiv.ringEquiv_symm_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Add β] [Mul β] (b : β) : (RingEquiv.symm e.ringEquiv) b = e.symm b

@[reducible, inline]

abbrev Equiv.nonUnitalNonAssocSemiring {α : Type u_1} {β : Type u_2} (e : α ≃ β) [NonUnitalNonAssocSemiring β] : NonUnitalNonAssocSemiring α

Transfer NonUnitalNonAssocSemiring across an Equiv

@[reducible, inline]

abbrev Equiv.nonUnitalSemiring {α : Type u_1} {β : Type u_2} (e : α ≃ β) [NonUnitalSemiring β] : NonUnitalSemiring α

Transfer NonUnitalSemiring across an Equiv

@[reducible, inline]

abbrev Equiv.addMonoidWithOne {α : Type u_1} {β : Type u_2} (e : α ≃ β) [AddMonoidWithOne β] : AddMonoidWithOne α

Transfer AddMonoidWithOne across an Equiv

@[reducible, inline]

abbrev Equiv.addGroupWithOne {α : Type u_1} {β : Type u_2} (e : α ≃ β) [AddGroupWithOne β] : AddGroupWithOne α

Transfer AddGroupWithOne across an Equiv

@[reducible, inline]

abbrev Equiv.nonAssocSemiring {α : Type u_1} {β : Type u_2} (e : α ≃ β) [NonAssocSemiring β] : NonAssocSemiring α

Transfer NonAssocSemiring across an Equiv

@[reducible, inline]

abbrev Equiv.semiring {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Semiring β] : Semiring α

Transfer Semiring across an Equiv

@[reducible, inline]

abbrev Equiv.nonUnitalCommSemiring {α : Type u_1} {β : Type u_2} (e : α ≃ β) [NonUnitalCommSemiring β] : NonUnitalCommSemiring α

Transfer NonUnitalCommSemiring across an Equiv

@[reducible, inline]

abbrev Equiv.commSemiring {α : Type u_1} {β : Type u_2} (e : α ≃ β) [CommSemiring β] : CommSemiring α

Transfer CommSemiring across an Equiv

@[reducible, inline]

abbrev Equiv.nonUnitalNonAssocRing {α : Type u_1} {β : Type u_2} (e : α ≃ β) [NonUnitalNonAssocRing β] : NonUnitalNonAssocRing α

Transfer NonUnitalNonAssocRing across an Equiv

@[reducible, inline]

abbrev Equiv.nonUnitalRing {α : Type u_1} {β : Type u_2} (e : α ≃ β) [NonUnitalRing β] : NonUnitalRing α

Transfer NonUnitalRing across an Equiv

@[reducible, inline]

abbrev Equiv.nonAssocRing {α : Type u_1} {β : Type u_2} (e : α ≃ β) [NonAssocRing β] : NonAssocRing α

Transfer NonAssocRing across an Equiv

@[reducible, inline]

abbrev Equiv.ring {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Ring β] : Ring α

Transfer Ring across an Equiv

@[reducible, inline]

abbrev Equiv.nonUnitalCommRing {α : Type u_1} {β : Type u_2} (e : α ≃ β) [NonUnitalCommRing β] : NonUnitalCommRing α

Transfer NonUnitalCommRing across an Equiv

@[reducible, inline]

abbrev Equiv.commRing {α : Type u_1} {β : Type u_2} (e : α ≃ β) [CommRing β] : CommRing α

Transfer CommRing across an Equiv

theorem Equiv.isDomain {α : Type u_1} {β : Type u_2} [Semiring β] [IsDomain β] (e : α ≃ β) : IsDomain α

Transfer IsDomain across an Equiv