hrmacbeth/math2001

Issues

• Is exercise 1.3.16 actually possible?

  #27 opened 13 days ago by zli117
  2

• Solution for "Or" and proof by cases 2.4.5 exercises (the last one)

  #26 opened a month ago by lukaIvanic
  3

• typo example 2.5.2

  #25 opened 4 months ago by rzeta0
  1

• improve example 2.4.4 with focussing dots

  #24 opened 4 months ago by rzeta0
  0

• Possible bug in `cancel` tactic?

  #17 opened 7 months ago by jdfm
  2

• typo in 2.3.6 ex 4

  #23 opened 4 months ago by rzeta0
  0

• Where to look for theorem or tactics?

  #22 opened 5 months ago by jiamingkong
  1

• 9.2.6 example

  #21 opened 5 months ago by ketilwright
  0

• possible copy/paste errors in 07_Euclidean_Algorithm.lean

  #20 opened 5 months ago by ketilwright
  0

• first use of `le_or_gt`

  #19 opened 6 months ago by mcol
  0

• further reading on transitioning from `extra` to `positivity` tactic

  #18 opened 6 months ago by rzeta0
  0

• exercises 1.3.11 (10) and (15) not possible using given tactics?

  #15 opened 7 months ago by rzeta0
  2

• Homework 7 problem 1 (small) typo

  #14 opened 8 months ago by dfpetrin
  1

• Homework 4 problem 2 typo

  #13 opened 8 months ago by dfpetrin
  1

• Unable to run locally

  #6 opened a year ago by arbitrary-dev
  22

• typeclass instance problem is stuck, it is often due to metavariables

  #8 opened a year ago by grindingpeon
  1

• A couple of typos

  #4 opened a year ago by zhassan-aws
  2

• Question: How is Lean automatically graded?

  #2 opened a year ago by Seasawher
  1