MIL/C09_Groups_and_Rings/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

49 declarations, 6 contain sorry, 0 declared as axioms

Imports (5)
Imported by 1 file
  1. example (example at line 9) line 9 source
  2. example (example at line 11) line 11 source
  3. example (example at line 13) line 13 source
  4. example (example at line 15) line 15 source
  5. example (example at line 17) line 17 source
  6. example (example at line 19) line 19 source
  7. example (example at line 22) line 22 source
  8. example (example at line 25) line 25 source
  9. example (example at line 27) line 27 source
  10. example (example at line 30) line 30 source
  11. example (example at line 34) line 34 source
  12. example (example at line 38) line 38 source
  13. example (example at line 45) line 45 source
  14. example (example at line 47) line 47 source
  15. example (example at line 50) line 50 source
  16. example (example at line 52) line 52 source
  17. example (example at line 54) line 54 source
  18. example (example at line 58) line 58 source
  19. example (example at line 62) line 62 source
  20. example (example at line 65) line 65 source
  21. example (example at line 71) line 71 source
  22. def chineseMap The homomorphism from R ⧸ ⨅ i, I i to Π i, R ⧸ I i featured in the Chinese Remainder Theorem sorry line 84 source

    Source documentation

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

    depends on sorry what this means

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

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    21 instances, coercions and auxiliary constants left out.

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

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

    depends on sorry what this means

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

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    37 instances, coercions and auxiliary constants left out.

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

  24. lemma chineseMap_mk' sorry line 91 source

    depends on sorry what this means

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

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    35 instances, coercions and auxiliary constants left out.

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

  25. lemma chineseMap_inj sorry line 97 source

    depends on sorry what this means

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

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    25 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C09_Groups_and_Rings/solutions/Solutions_S02_Rings.lean:32 (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.

  26. theorem isCoprime_Inf sorry line 109 source

    depends on sorry 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 28 more

    58 instances, coercions and auxiliary constants left out.

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

    Tactic trace: 7 steps

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

  27. lemma chineseMap_surj sorry line 124 source

    depends on sorry 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, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat, Exists.intro, Finset.sum, Finset.univ and 4 more

    51 instances, coercions and auxiliary constants left out.

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

    Tactic trace: 11 steps

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

  28. def chineseIso line 138 source

    depends on sorry 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/solutions/Solutions_S02_Rings.lean:75 (same declaration text).

    Tactic trace: 21 steps

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

  29. example (example at line 145) line 145 source
  30. example (example at line 149) line 149 source
  31. example (example at line 156) line 156 source
  32. example (example at line 158) line 158 source
  33. example (example at line 160) line 160 source
  34. example (example at line 164) line 164 source
  35. example (example at line 166) line 166 source
  36. example (example at line 168) line 168 source
  37. example (example at line 172) line 172 source
  38. example (example at line 176) line 176 source
  39. example (example at line 180) line 180 source
  40. example (example at line 182) line 182 source
  41. example (example at line 184) line 184 source
  42. example (example at line 186) line 186 source
  43. example (example at line 189) line 189 source
  44. example (example at line 193) line 193 source
  45. example (example at line 197) line 197 source
  46. example (example at line 211) line 211 source

    Source comment

    Mathlib knows about D'Alembert-Gauss theorem: ``ℂ`` is algebraically closed.
    example : IsAlgClosed ℂ := inferInstance
…
  47. example (example at line 215) line 215 source
  48. def circleEquation line 219 source

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

    Statement uses: MvPolynomial, Fin, OfNat.ofNat, Nat, Real

    Proof uses: HSub.hSub, Finsupp, HAdd.hAdd, HPow.hPow, MvPolynomial.X

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  49. example (example at line 221) line 221 source