Documentation

Mathlib.Algebra.Field.TransferInstance

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 β] :

Transfer NNRatCast across an Equiv

Equations
    Instances For
      @[reducible, inline]
      abbrev Equiv.ratCast {α : Type u_1} {β : Type u_2} (e : α β) [RatCast β] :

      Transfer RatCast across an Equiv

      Equations
        Instances For
          @[reducible, inline]
          abbrev Equiv.divisionRing {α : Type u_1} {β : Type u_2} (e : α β) [DivisionRing β] :

          Transfer DivisionRing across an Equiv

          Equations
            Instances For
              @[reducible, inline]
              abbrev Equiv.field {α : Type u_1} {β : Type u_2} (e : α β) [Field β] :

              Transfer Field across an Equiv

              Equations
                Instances For