Theorems · Definition · commutative algebra
Prime
{M : Type u_1} → [CommMonoidWithZero M] → M → PropAn element p of a commutative monoid with zero (e.g., a ring) is called prime,
if it's not zero, not a unit, and p ∣ a * b → p ∣ a ∨ p ∣ b for all a, b.
- Defined in
- Mathlib.Algebra.Prime.Defs
- Cited by
- 277 results in Mathlib
- Foundations
- Depth 6 from the axioms, rests on 59 definitions · uses no axioms
- Assumes
- CommMonoidWithZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- IsUnitproof · cited by 1,602
- CommMonoidWithZerostatement and proof · cited by 913
Cited by285
Results whose statement or proof uses this declaration.
- IsPrimePowproof · cited by 77
- Prime.irreduciblestatement and proof · cited by 54
- Prime.ne_zerostatement and proof · cited by 47
- Prime.not_isUnitstatement and proof · cited by 29
- Ideal.span_singleton_primestatement · cited by 27
- Nat.prime_iff_prime_intstatement and proof · cited by 27
- UniqueFactorizationMonoid.prime_of_normalized_factorstatement and proof · cited by 23
- Nat.prime_iffstatement · cited by 20
- Nat.Prime.primestatement · cited by 19
- Prime.dvd_or_dvdstatement and proof · cited by 17
- Ideal.isPrime_of_primestatement and proof · cited by 17
- Ideal.prime_of_isPrimestatement · cited by 15
Showing the 200 most cited of 285.