Learning path

Each declaration appears after its prerequisites.

  1. easy These are proofs of propositions
  2. MyRing.add_zero a + 0 = a in any ring, from commutativity and zero_add
  3. MyRing.add_neg_cancel_right@MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean Prove these:
  4. MyRing.add_left_cancel@MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean Exercise: left cancellation of addition (sorry)
  5. MyRing.mul_zero a * 0 = 0 via cancellation
  6. C03S01.my_lemma Exercise: a universally quantified statement (sorry)
  7. C03S06.ConvergesTo Convergence of a real sequence
  8. C03S06.convergesTo_const A constant sequence converges to its constant after C03S06.ConvergesTo
  9. C03S01.my_lemma4@MIL/C03_Logic/solutions/Solutions_S01_Implication_and_the_Universal_Quantifier.lean Solution: |x*y| < epsilon by a calc chain
  10. C03S06.convergesTo_add@MIL/C03_Logic/solutions/Solutions_S06_Sequences_and_Convergence.lean The limit of a sum is the sum of the limits after C03S06.ConvergesTo
  11. Cantor@MIL/C04_Sets_and_Functions/solutions/Solutions_S02_Functions.lean Cantor: no function from α to its power set is surjective
  12. PropForm.subst_eq_of_not_mem_vars' alternative proof:
  13. PropForm.subst_eval_eq' alternative proof:
  14. C06S02.Point fill in the rest
  15. chineseMap@MIL/C09_Groups_and_Rings/S02_Rings.lean The homomorphism from R ⧸ ⨅ i, I i to Π i, R ⧸ I i featured in the Chinese Remainder Theorem
  16. chineseMap@MIL/C09_Groups_and_Rings/solutions/Solutions_S02_Rings.lean The homomorphism from R ⧸ ⨅ i, I i to Π i, R ⧸ I i featured in the Chinese Remainder Theorem