MIL/C09_Groups_and_Rings/solutions/Solutions_S02_Rings.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned Mathematics in Lean documentation, Pinned Mathematics in Lean textbook

7 declarations, 0 contain sorry, 0 declared as axioms

Imports (5)
  1. def chineseMap The homomorphism from R ⧸ ⨅ i, I i to Π i, R ⧸ I i featured in the Chinese Remainder Theorem line 20 source

    Source documentation

    The homomorphism from R ⧸ ⨅ i, I i to Π i, R ⧸ I i featured in the Chinese Remainder Theorem.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, Ideal, RingHom, HasQuotient.Quotient, iInf

    Proof uses: Ideal.Quotient.lift, Pi.ringHom, Ideal.Quotient.mk

    25 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C09_Groups_and_Rings/S02_Rings.lean:84 (same statement text; different proof or body). Qualify references as chineseMap@path.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    def chineseMap (I : ι → Ideal R) : (R ⧸ ⨅ i, I i) →+* Π i, R ⧸ I i :=
…
  2. lemma chineseMap_mk line 24 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, Ideal, Eq, HasQuotient.Quotient, RingHom, iInf, chineseMap, Quotient.mk, Submodule.quotientRel, Ideal.Quotient.mk

    Proof uses: rfl

    33 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C09_Groups_and_Rings/S02_Rings.lean:87 (same statement text; different proof or body). Qualify references as chineseMap_mk@path.

  3. lemma chineseMap_mk' line 28 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, Ideal, Eq, HasQuotient.Quotient, RingHom, iInf, chineseMap, Ideal.Quotient.mk

    Proof uses: rfl

    34 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C09_Groups_and_Rings/S02_Rings.lean:91 (same statement text; different proof or body). Qualify references as chineseMap_mk'@path.

  4. lemma chineseMap_inj line 32 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, Ideal, Function.Injective, HasQuotient.Quotient, iInf, RingHom, chineseMap

    Proof uses: Eq.mpr, Ideal.Quotient.lift, Pi.ringHom, Ideal.Quotient.mk, id, Eq, congrArg, chineseMap.eq_1, RingHom.ker, propext, Ideal.injective_lift_iff, Ideal.ker_Pi_Quotient_mk, Eq.refl

    34 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C09_Groups_and_Rings/S02_Rings.lean:97 (same statement text; different proof or body). Qualify references as chineseMap_inj@path.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  5. theorem isCoprime_Inf line 35 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, Ideal, Finset, Membership.mem, IsCoprime, iInf

    Proof uses: Eq.mpr, Eq, HAdd.hAdd, OfNat.ofNat, id, Finset.induction, Classical.propDecidable, EmptyCollection.emptyCollection, of_eq_true, Eq.trans, Top.top, True, congr, congrArg, funext, False, iInf_congr_Prop, Iff.of_eq, Eq.refl, iInf_neg and 49 more

    83 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C09_Groups_and_Rings/S02_Rings.lean:109 (same statement text; different proof or body). Qualify references as isCoprime_Inf@path.

    Tactic trace: 12 steps

    Open to load the checked before-and-after goal states.

  6. lemma chineseMap_surj line 52 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, Fintype, Ideal, Ne, IsCoprime, Function.Surjective, HasQuotient.Quotient, iInf, RingHom, chineseMap

    Proof uses: Eq, Ideal.Quotient.mk, Exists, And, OfNat.ofNat, Membership.mem, Finset, Compl.compl, Classical.propDecidable, Singleton.singleton, id, Eq.mp, Not, Eq.trans, congrArg, HAdd.hAdd, Iff.mp, Ideal.isCoprime_iff_exists, isCoprime_Inf, Submodule and 35 more

    93 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C09_Groups_and_Rings/S02_Rings.lean:124 (same statement text; different proof or body). Qualify references as chineseMap_surj@path.

    Tactic trace: 26 steps

    Open to load the checked before-and-after goal states.

  7. def chineseIso line 75 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, Fintype, Ideal, Ne, IsCoprime, RingEquiv, HasQuotient.Quotient, iInf

    Proof uses: Equiv, Equiv.ofBijective, RingHom, chineseMap, RingEquiv.mk

    38 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C09_Groups_and_Rings/S02_Rings.lean:138 (same declaration text).