Mathlib Map

Structures · Algebra

IsDomain

A domain is a nontrivial semiring such that multiplication by a nonzero element is cancellative on both sides. In other words, a nontrivial semiring R satisfying ∀ {a b c : R}, a ≠ 0 → a * b = a * c → b = c and ∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c. This is implemented as a mixin for Semiring α. To obtain an integral domain use [CommRing α] [IsDomain α].

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

Extends2

Extended by1

Concrete types that are instances35

  • Int
  • Nat
  • Real
  • Rat
  • ZMod
  • Polynomial
  • CommRingCat.carrier
  • Quaternion
  • HahnSeries
  • PadicInt
  • MonoidAlgebra
  • AddMonoidAlgebra
  • Zsqrtd
  • Localization
  • ArchimedeanClass.FiniteElement
  • WittVector
  • NumberField.RingOfIntegers
  • Ring.NormalClosure
  • CyclotomicRing
  • AlgebraicGeometry.ValuativeCommSq.R
  • SymmetricAlgebra
  • FreeAlgebra
  • TensorAlgebra
  • MvPolynomial
  • PowerSeries
  • WeierstrassCurve.Affine.CoordinateRing
  • Localization.AtPrime
  • Subtype
  • OrderDual
  • MulOpposite
  • Lex
  • AddOpposite
  • HasQuotient.Quotient
  • Shrink
  • Ideal

How is a type an instance?

Loading the hierarchy index…

Assumed by2,486

Ancestors5