Mathlib Map

Structures · Algebra

Ideal.IsPrime

An ideal P of a ring R is prime if P ≠ R and xy ∈ P → x ∈ P ∨ y ∈ P

Defined in
Mathlib.RingTheory.Ideal.Prime
Shape
One type argument · adds ne_top', mem_or_mem'
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by1

Concrete types that are instances5

  • Polynomial
  • NumberField.RingOfIntegers
  • MvPolynomial
  • Subtype
  • HasQuotient.Quotient

How is a type an instance?

Loading the hierarchy index…

Assumed by616

Ancestors0

No ancestors.