Structures · Algebra

Ring

A Ring is a Semiring with negation making it an additive group.

Defined in: Mathlib.Algebra.Ring.Defs
Shape: One type argument · adds sub_eq_add_neg, zsmul_zero', zsmul_succ', zsmul_neg', neg_add_cancel, intCast_ofNat, intCast_negSucc

Extends3

Every Ring is also a

Int
Real
Complex
SeparationQuotient
CategoryTheory.Functor.obj
ContinuousLinearMap
Polynomial
Filter.Germ
BoundedContinuousFunction
Padic
CStarMatrix
UniformSpace.Completion
TensorProduct
Quaternion
Unitization
WithConv
Matrix
WithVal
HahnSeries
LocallyConstant
DomMulAct
WithLp
MeasureTheory.SimpleFunc
FreeAbelianGroup
MonoidAlgebra
RestrictedProduct
TrivSqZeroExt
AddMonoidAlgebra
DirectLimit
DirectSum
RestrictScalars
DoubleCentralizer
Zsqrtd
DomAddAct
SkewMonoidAlgebra
CauSeq.Completion.Cauchy
ContMDiffMap
LocalizedModule
OreLocalization
PiTensorProduct
QuaternionAlgebra
CategoryTheory.Limits.Cone.pt
PreLp
CauSeq
ContinuousLinearMapWOT
LucasLehmer.X
CategoryTheory.End
MvPowerSeries
FreeRing
Module.End
CliffordAlgebra
RingCon.Quotient
RingQuot
MulActionHom
Perfection
Ring.DirectLimit
RingCat.carrier
CentroidHom
WithIdealFilter
IsIdempotentElem.Corner
FreeAlgebra
SemiRingCat.carrier
AddMonoid.End
TensorAlgebra
IncidenceAlgebra
RingCat.Colimits.ColimitType
NumberField.mixedEmbedding.euclidean.mixedSpace
UniversalEnvelopingAlgebra
AlgCat.carrier
SkewPolynomial
GradedTensorProduct
BialgCat.carrier
HopfAlgCat.carrier
CategoryTheory.Abelian.FreydMitchell.EmbeddingRing
CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.EmbeddingRing
Subtype
Prod
OrderDual
Set.Elem
ULift
MulOpposite
Lex
AddOpposite
HasQuotient.Quotient
ContinuousMap
Shrink
WithAbs

Loading the hierarchy index…