Divisibility in integral domains

• Irreducible elements

ClassInvertible elements#

Invertible a gives a two-sided multiplicative inverse of a.

Invertible.{u} {α : Type u} [Mul α] [One α] (a : α) : Type u

Sources

• Mathlib documentation: Invertible
• Source of Invertible in Mathlib/Algebra/Group/Invertible/Defs.lean
• Mathlib undergraduate list: Ring Theory › Divisibility in integral domains

MathlibInvertible

Uses 1 · Used by 16

Statement usesNatural number

Used byDirichlet’s Theorem · Product of Segments of Chords · The Solution of a Cubic · The Solution of the General Quartic Equation · General linear group as a Lie group · Urysohn's lemma · Binomial inverse theorem · Sylvester's determinant theorem · Apollonius's theorem · British flag theorem · Intersecting secants theorem · Tangent-secant theorem · Thales's theorem · Complex classification · Sylvester's law of inertia (existence) · General linear group (Classical automorphism groups)

• Coprime elements
• Unique factorisation domain (UFD)
• Greatest common divisor
• Least common multiple
• \(A\[{X_i}\]\) is a UFD when \(A\) is a UFD
• Principal ideal domain
• Euclidean rings
• Euclid's' algorithm

Instance\(\Z\) is a Euclidean ring#

Mathlib states this as Int.euclideanDomain.

Int.euclideanDomain : EuclideanDomain ℤ

Sources

• Mathlib documentation: Int.euclideanDomain
• Source of Int.euclideanDomain in Mathlib/Algebra/EuclideanDomain/Int.lean
• Mathlib undergraduate list: Ring Theory › Divisibility in integral domains

MathlibInt.euclideanDomain

Uses 2 · Used by 1

Statement usesEuclidean domain · Ring structure \(\Z\)

Used byFormula for Pythagorean Triples

DefinitionCongruence in \(\Z\)#

a ≡ b [ZMOD n] when a % n = b % n.

Int.ModEq (n a b : ℤ) : Prop

Sources

• Mathlib documentation: Int.ModEq
• Source of Int.ModEq in Mathlib/Data/Int/ModEq.lean
• Mathlib undergraduate list: Ring Theory › Divisibility in integral domains

MathlibInt.ModEq

Uses 1 · Used by 7

Statement usesInteger

Used byLucas-Lehmer primality test · Third Sylow theorem · Matiyasevič's theorem · Quadratic reciprocity · Sum of four squares · Sum of two squares · Lucas's theorem

DefinitionPrime numbers#

An 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.

Prime.{u_1} {M : Type u_1} [CommMonoidWithZero M] (p : M) : Prop

Sources

• Mathlib documentation: Prime
• Source of Prime in Mathlib/Algebra/Prime/Defs.lean
• Mathlib undergraduate list: Ring Theory › Divisibility in integral domains

MathlibPrime

Uses 1 · Used by 15

Statement usesNatural number

Used byLucas-Lehmer primality test · Unique factorisation domain · Frobenius morphism · Classification of abelian simple groups · First Sylow theorem · Structure of finitely generated abelian groups · Third Sylow theorem · Arithmetic functions · Hensel's lemma (for \(\mathbb{Z}_p\)) · Quadratic reciprocity · Ring of Witt vectors · Sum of four squares · Sum of two squares · \(p\)-adic integer · \(p\)-adic number

TheoremBézout's identity#

Bézout's lemma

exists_gcd_eq_mul_add_mul.{u} {R : Type u} [CommRing R] [IsBezout R] [IsDomain R] [GCDMonoid R]
  (a b : R) : ∃ x y, gcd a b = a * x + b * y

Sources

• Mathlib documentation: exists_gcd_eq_mul_add_mul
• Source of exists_gcd_eq_mul_add_mul in Mathlib/RingTheory/PrincipalIdealDomain.lean
• Mathlib undergraduate list: Ring Theory › Divisibility in integral domains

Mathlibexists_gcd_eq_mul_add_mul

Uses 5

Statement usesFinite set · Greatest common divisor · Principal ideal domain

Proof usesInteger · Sum of subspaces

Definition\(\Z/n\Z\) and its invertible elements#

unitOfCoprime makes an element of (ZMod n)ˣ given a natural number x and a proof that x is coprime to n

ZMod.unitOfCoprime {n : ℕ} (x : ℕ) (h : x.Coprime n) : (ZMod n)ˣ

Sources

• Mathlib documentation: ZMod.unitOfCoprime
• Source of ZMod.unitOfCoprime in Mathlib/Data/ZMod/Basic.lean
• Mathlib undergraduate list: Ring Theory › Divisibility in integral domains

MathlibZMod.unitOfCoprime

Uses 2 · Used by 1

Statement usesInteger · Ring

Used byEuler's totient function (\(\varphi\))

• Euler's totient function (\(\varphi\))

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.