Documentation

Mathlib.Analysis.Normed.Ring.TransferInstance

Transfer normed algebraic structures across Equivs #

In this file, we transfer a (semi-)normed ring structure across an equivalence. This continues the pattern set in Mathlib/Algebra/Module/TransferInstance.lean.

@[reducible, inline]
abbrev Equiv.seminormedRing {α : Type u_1} {β : Type u_2} [SeminormedRing β] (e : α ≃ β) :

Transfer a SeminormedRing across an Equiv

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

      Transfer a NormedRing across an Equiv

      Equations
        Instances For