Code

added Linear.Order#300

Code

Merged

jjdishere merged 37 commits intojjdishere:masterjjdishere/EG:masterfrom xyzw12345:masterxyzw12345/EG:masterCopy head branch name to clipboardJan 22, 2024

+1,498-139

Commits

Commits on Dec 26, 2023

• upd congr_ex_6&7

  xyzw12345

  committed
  a09c167

  Copy full SHA for a09c167

Commits on Dec 27, 2023

• Update Congruence_exercise_ygr_7.lean

  xyzw12345

  committed
  704cfc6

  Copy full SHA for 704cfc6

• finished prove of congr_exercise_ygr_6

  xyzw12345

  committed
  77a8789

  Copy full SHA for 77a8789

• modify several thm in trash

  xyzw12345

  committed
  68d6cf9

  Copy full SHA for 68d6cf9

Commits on Dec 28, 2023

• upd proof of 7

  xyzw12345

  committed
  20ceda5

  Copy full SHA for 20ceda5

Commits on Dec 29, 2023

• upd on Congr_ex_ygr_7

  xyzw12345

  committed
  431e91d

  Copy full SHA for 431e91d

Commits on Jan 12, 2024

• Merge remote-tracking branch 'upstream/master'

  xyzw12345

  committed
  8b1b370

  Copy full SHA for 8b1b370

• merge from upstream and lean upd 20240112

  xyzw12345

  committed
  66f3bed

  Copy full SHA for 66f3bed

Commits on Jan 14, 2024

• upd problem_5 line_trash

  Show description for 158e77d
  xyzw12345

  committed
  158e77d

  Copy full SHA for 158e77d

• Update Problem_5.lean

  xyzw12345

  committed
  48020a0

  Copy full SHA for 48020a0

• Merge remote-tracking branch 'upstream/master'

  xyzw12345

  committed
  3894701

  Copy full SHA for 3894701

• upd on problem 5 and open Order.lean

  xyzw12345

  committed
  17dd623

  Copy full SHA for 17dd623

• Update Order.lean

  xyzw12345

  committed
  d0d91a4

  Copy full SHA for d0d91a4

Commits on Jan 15, 2024

• Update Problem_5.lean

  xyzw12345

  committed
  6057bf5

  Copy full SHA for 6057bf5

• Merge remote-tracking branch 'upstream/master'

  xyzw12345

  committed
  f4878cb

  Copy full SHA for f4878cb

• upd 20240115

  xyzw12345

  committed
  f7c4b20

  Copy full SHA for f7c4b20

Commits on Jan 16, 2024

• upd on problem_11 and Order.lean

  xyzw12345

  committed
  f5653e7

  Copy full SHA for f5653e7

• Update Order.lean

  xyzw12345

  committed
  723fe56

  Copy full SHA for 723fe56

Commits on Jan 17, 2024

• upd order.lean

  xyzw12345

  committed
  d30bd7b

  Copy full SHA for d30bd7b

• Merge remote-tracking branch 'upstream/master'

  xyzw12345

  committed
  e163b88

  Copy full SHA for e163b88

• Update Order.lean

  xyzw12345

  committed
  3a7f097

  Copy full SHA for 3a7f097

Commits on Jan 19, 2024

• Update Order.lean

  Show description for db22734
  xyzw12345

  committed
  db22734

  Copy full SHA for db22734

• Update Order.lean

  Show description for 2478bed
  xyzw12345

  committed
  2478bed

  Copy full SHA for 2478bed

• Update Order.lean

  Show description for 4ff28d2
  xyzw12345

  committed
  4ff28d2

  Copy full SHA for 4ff28d2

• Merge remote-tracking branch 'upstream/master'

  xyzw12345

  committed
  8557e43

  Copy full SHA for 8557e43

• update Order.lean

  Show description for 9a4841e
  xyzw12345

  committed
  9a4841e

  Copy full SHA for 9a4841e

Commits on Jan 21, 2024

• Update Order.lean

  xyzw12345

  committed
  2dbce01

  Copy full SHA for 2dbce01

• Update Order.lean

  Show description for a0306a0
  xyzw12345

  committed
  a0306a0

  Copy full SHA for a0306a0

• Update Order.lean

  Show description for 38f5f90
  xyzw12345

  committed
  38f5f90

  Copy full SHA for 38f5f90

• Update Order.lean

  Show description for 264b945
  xyzw12345

  committed
  264b945

  Copy full SHA for 264b945

• Update Order.lean

  Show description for 2bc8c3c
  xyzw12345

  committed
  2bc8c3c

  Copy full SHA for 2bc8c3c

• Update Order.lean

  Show description for a83b164
  xyzw12345

  committed
  a83b164

  Copy full SHA for a83b164

• Update Order.lean

  Show description for 25c7dfb
  xyzw12345

  committed
  25c7dfb

  Copy full SHA for 25c7dfb

• Update Order.lean

  Show description for 8bec8e7
  xyzw12345

  committed
  8bec8e7

  Copy full SHA for 8bec8e7

• Merge remote-tracking branch 'upstream/master'

  xyzw12345

  committed
  b04e497

  Copy full SHA for b04e497

• upd before PR

  Show description for 2626a37
  xyzw12345

  committed
  2626a37

  Copy full SHA for 2626a37

• Update Line.lean

  xyzw12345

  committed
  211cffb

  Copy full SHA for 211cffb