Mathlib Map

Structures · Analysis

NormedCommRing

A normed commutative ring is a 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 NormedCommRing is also a

Provided automatically by

Concrete types that are instances15

  • Int
  • Real
  • SeparationQuotient
  • BoundedContinuousFunction
  • UniformSpace.Completion
  • PadicInt
  • TrivSqZeroExt
  • RestrictScalars
  • Subtype
  • Prod
  • ULift
  • MulOpposite
  • PUnit
  • HasQuotient.Quotient
  • ContinuousMap

How is a type an instance?

Loading the hierarchy index…

Assumed by241

Ancestors128