Mathlib Map

Structures · Analysis

NonUnitalNormedCommRing

A non-unital normed commutative ring is a non-unital commutative ring endowed with a norm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖.

Defined in
Mathlib.Analysis.Normed.Ring.Basic
Shape
One type argument · adds mul_comm
Open in Mathlib docs

Extends2

Extended by2

Forgetful instances

Every NonUnitalNormedCommRing is also a

Provided automatically by

Concrete types that are instances10

  • SeparationQuotient
  • BoundedContinuousFunction
  • RestrictScalars
  • ContinuousMapZero
  • ZeroAtInftyContinuousMap
  • Subtype
  • Prod
  • ULift
  • MulOpposite
  • ContinuousMap

How is a type an instance?

Loading the hierarchy index…

Assumed by15

Ancestors93