Transfer algebraic structures across Equivs

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

@[reducible, inline]

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

Transfer NNRatCast across an Equiv

Equations

• e.nnratCast = { nnratCast := fun (q : ℚ≥0) => e.symm ↑q }

@[reducible, inline]

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

Transfer RatCast across an Equiv

Equations

• e.ratCast = { ratCast := fun (n : ℚ) => e.symm ↑n }

@[reducible, inline]

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

Transfer DivisionRing across an Equiv

Equations

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

@[reducible, inline]

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

Transfer Field across an Equiv

Equations

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