Fundamentals

• Ring
• Subrings
• Ring morphisms

InstanceRing structure \(\Z\)#

Mathlib states this as Int.instCommRing.

Int.instCommRing : CommRing ℤ

Sources

• Mathlib documentation: Int.instCommRing
• Source of Int.instCommRing in Mathlib/Algebra/Ring/Int/Defs.lean
• Mathlib undergraduate list: Ring Theory › Fundamentals

MathlibInt.instCommRing

Uses 2 · Used by 19

Statement usesInteger · Ring

Used byLiouville’s Theorem and the Construction of Transcendental Numbers · The Ballot Problem · Derangements Formula · Principle of Inclusion/Exclusion · The Friendship Theorem · The Fundamental Theorem of Arithmetic · Erdős–Ginzburg–Ziv theorem · Focal subgroup theorem · Lie's theorem · Abel's theorem · Dirichlet's approximation theorem · Dirichlet's unit theorem · Glaisher's theorem · Lucas's theorem · Mahler's theorem · Pentagonal number theorem · Von Staudt–Clausen theorem · \(\Z\) is a Euclidean ring · Differentiability of the limit of a sequence of functions

InstanceProduct of rings#

Mathlib states this as Pi.ring.

Pi.ring.{u, v} {I : Type u} {f : I → Type v} [(i : I) → Ring (f i)] : Ring ((i : I) → f i)

Sources

• Mathlib documentation: Pi.ring
• Source of Pi.ring in Mathlib/Algebra/Ring/Pi.lean
• Mathlib undergraduate list: Ring Theory › Fundamentals

MathlibPi.ring

Uses 2 · Used by 1

Statement usesInteger · Ring

Used byChinese remainder theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.