NYLL
Module

QuotientProducts.lean

Nyll.SchemeTheory.Pi1.RingTheory.QuotientProducts
1 declaration indexed from sourceView source ↗

Module documentation

Quotient products for coprime ideals

The canonical equivalence from a quotient by the infimum of pairwise coprime ideals sends a quotient representative to its family of representatives in the individual quotients.

Imports1
  • Mathlib.RingTheory.Ideal.Quotient.Operations
Imported by2

Declarations

lemma

quotientInfRingEquivPiQuotient_mk

L32 ↗
Ideal.quotientInfRingEquivPiQuotient_mk
Source context 1 command

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
Lean source · full declaration
lemma Ideal.quotientInfRingEquivPiQuotient_mk {R ι : Type*} [Finite ι] [CommRing R]
    (I : ι → Ideal R) (hI : Pairwise (Function.onFun IsCoprime I)) (x : R) :
    Ideal.quotientInfRingEquivPiQuotient I hI x = fun _ ↦ Ideal.Quotient.mk _ x := rfl

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.