Mathlib Map

Structures · Algebra

CommRing

A commutative ring is a ring with commutative multiplication.

Defined in
Mathlib.Algebra.Ring.Defs
Shape
One type argument · adds mul_comm
Open in Mathlib docs

Extends2

Extended by5

Forgetful instances

Every CommRing is also a

Provided automatically by

Concrete types that are instances100

  • Int
  • Real
  • Rat
  • Quiver.Hom
  • Complex
  • TopCat.carrier
  • SeparationQuotient
  • CategoryTheory.Functor.obj
  • BitVec
  • ZMod
  • Polynomial
  • Filter.Germ
  • BoundedContinuousFunction
  • Padic
  • CommRingCat.carrier
  • RatFunc
  • UniformSpace.Completion
  • TensorProduct
  • Unitization
  • WithConv
  • WithVal
  • HahnSeries
  • LocallyConstant
  • DomMulAct
  • PadicInt
  • QuadraticAlgebra
  • MeasureTheory.SimpleFunc
  • FreeAbelianGroup
  • MonoidAlgebra
  • RestrictedProduct
  • TrivSqZeroExt
  • ModuleCat.carrier
  • AddMonoidAlgebra
  • DirectLimit
  • DirectSum
  • IsLocalRing.ResidueField
  • Polynomial.SplittingField
  • RestrictScalars
  • Zsqrtd
  • ZNum
  • DomAddAct
  • ArchimedeanClass.FiniteElement
  • CauSeq.Completion.Cauchy
  • AlgebraicClosure
  • PerfectClosure
  • ContMDiffMap
  • LocalizedModule
  • AdjoinRoot
  • OreLocalization
  • PiTensorProduct
  • CategoryTheory.Limits.Cone.pt
  • WittVector
  • NumberField.InfiniteAdeleRing
  • NumberField.RingOfIntegers
  • IsDedekindDomain.FiniteAdeleRing
  • CauSeq
  • TruncatedWittVector
  • LucasLehmer.X
  • NumberField.AdeleRing
  • TopCommRingCat.α
  • GaussianInt
  • MvPowerSeries
  • FreeRing
  • CompareReals.Q
  • Ring.NormalClosure
  • ArithmeticFunction
  • AdicCompletion
  • CyclotomicRing
  • AlgebraicGeometry.ValuativeCommSq.R
  • FreeCommRing
  • CliffordAlgebra
  • SymmetricAlgebra
  • AdicCompletion.AdicCauchySequence
  • RingCon.Quotient
  • HomogeneousLocalization
  • RingQuot
  • MulActionHom
  • Algebra.Presentation.Core
  • Perfection
  • Ring.DirectLimit
  • RingCat.carrier
  • PointedContMDiffMap
  • PreTilt
  • CommRingCat.Colimits.ColimitType
  • Poly
  • Algebra.Extension.Ring
  • IsIdempotentElem.Corner
  • Polynomial.UniversalFactorizationRing
  • StandardEtalePair.Ring
  • BDeRhamPlus
  • CommHopfAlgCat.X
  • CommBialgCat.carrier
  • CommAlgCat.carrier
  • Subtype
  • Prod
  • OrderDual
  • ULift
  • MulOpposite
  • PUnit
  • Lex

How is a type an instance?

Loading the hierarchy index…

Assumed by21,252

Ancestors94