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.

Equations

• e.ringEquiv = { toEquiv := e, map_mul' := ⋯, map_add' := ⋯ }

@[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

Equations

• e.nonUnitalNonAssocSemiring = Function.Injective.nonUnitalNonAssocSemiring ⇑e ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

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

Transfer NonUnitalSemiring across an Equiv

Equations

• e.nonUnitalSemiring = Function.Injective.nonUnitalSemiring ⇑e ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

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

Transfer AddMonoidWithOne across an Equiv

Equations

• e.addMonoidWithOne = { natCast := fun (n : ℕ) => e.invFun ↑n, toAddMonoid := e.addMonoid, toOne := e.one, natCast_zero := ⋯, natCast_succ := ⋯ }

@[reducible, inline]

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

Transfer AddGroupWithOne across an Equiv

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

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

Transfer NonAssocSemiring across an Equiv

Equations

• e.nonAssocSemiring = Function.Injective.nonAssocSemiring ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

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

Transfer Semiring across an Equiv

Equations

• e.semiring = Function.Injective.semiring ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

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

Transfer NonUnitalCommSemiring across an Equiv

Equations

• e.nonUnitalCommSemiring = Function.Injective.nonUnitalCommSemiring ⇑e ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

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

Transfer CommSemiring across an Equiv

Equations

• e.commSemiring = Function.Injective.commSemiring ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

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

Transfer NonUnitalNonAssocRing across an Equiv

Equations

• e.nonUnitalNonAssocRing = Function.Injective.nonUnitalNonAssocRing ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

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

Transfer NonUnitalRing across an Equiv

Equations

• e.nonUnitalRing = Function.Injective.nonUnitalRing ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

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

Transfer NonAssocRing across an Equiv

Equations

• e.nonAssocRing = Function.Injective.nonAssocRing ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

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

Transfer Ring across an Equiv

Equations

• e.ring = Function.Injective.ring ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

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

Transfer NonUnitalCommRing across an Equiv

Equations

• e.nonUnitalCommRing = Function.Injective.nonUnitalCommRing ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

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

Transfer CommRing across an Equiv

Equations

• e.commRing = Function.Injective.commRing ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Transfer IsDomain across an Equiv