Code

Congruence exercise ygr 1-4#272

Code

Merged

jjdishere merged 48 commits intojjdishere:masterjjdishere/EG:masterfrom Thmoas-Guan:masterThmoas-Guan/EG:masterCopy head branch name to clipboardJan 12, 2024

+1,547-85

Commits

Commits on Nov 19, 2023

• Merge pull request #2 from Thmoas-Guan/master

  Show description for 15117af
  Mosente

  authored
  15117af

  Copy full SHA for 15117af

Commits on Nov 25, 2023

• 1

  Mosente

  committed
  de79914

  Copy full SHA for de79914

• Merge remote-tracking branch 'upstream/master'

  Mosente

  committed
  ee5031f

  Copy full SHA for ee5031f

• Update Problem1.4.lean

  Mosente

  committed
  5d218e2

  Copy full SHA for 5d218e2

Commits on Nov 26, 2023

• save

  Mosente

  committed
  85fc835

  Copy full SHA for 85fc835

• save

  Mosente

  committed
  6d6e13a

  Copy full SHA for 6d6e13a

Commits on Dec 1, 2023

• 12.1

  Mosente

  committed
  45017e3

  Copy full SHA for 45017e3

• Merge remote-tracking branch 'upstream/master'

  Mosente

  committed
  f825388

  Copy full SHA for f825388

• Update Problem1.2.lean

  Mosente

  committed
  c8fe79f

  Copy full SHA for c8fe79f

Commits on Dec 9, 2023

• Merge remote-tracking branch 'upstream/master'

  Mosente

  committed
  ea5a666

  Copy full SHA for ea5a666

Commits on Dec 10, 2023

• 20231210

  Mosente

  committed
  54dd375

  Copy full SHA for 54dd375

Commits on Dec 14, 2023

• Merge remote-tracking branch 'upstream/master'

  Mosente

  committed
  0f74d2f

  Copy full SHA for 0f74d2f

• Update Ray_trash.lean

  Mosente

  committed
  57211d1

  Copy full SHA for 57211d1

• Merge remote-tracking branch 'upstream/master'

  Mosente

  committed
  2994ba1

  Copy full SHA for 2994ba1

Commits on Dec 16, 2023

• refine 1.1 1.3

  Thmoas-Guan

  committed
  34f0fa3

  Copy full SHA for 34f0fa3

• Merge remote-tracking branch 'upstream/master'

  Thmoas-Guan

  committed
  9f1a38b

  Copy full SHA for 9f1a38b

• 12.16 refine

  Thmoas-Guan

  committed
  8a7ae43

  Copy full SHA for 8a7ae43

• 1216

  Mosente

  committed
  ed120ed

  Copy full SHA for ed120ed

Commits on Dec 17, 2023

• Congruence exercise ygr3

  Thmoas-Guan

  committed
  7caf32f

  Copy full SHA for 7caf32f

• Merge remote-tracking branch 'upstream/master'

  Thmoas-Guan

  committed
  3da8071

  Copy full SHA for 3da8071

• Merge pull request #5 from Mosente/master

  Show description for 8a67e83
  Thmoas-Guan

  authored
  8a67e83

  Copy full SHA for 8a67e83

• ygr 1,3,in the new folder

  Thmoas-Guan

  committed
  4dc732b

  Copy full SHA for 4dc732b

• 12.17final

  Thmoas-Guan

  committed
  dce7aba

  Copy full SHA for dce7aba

Commits on Dec 18, 2023

• theorem index for ygr

  Thmoas-Guan

  committed
  98722d5

  Copy full SHA for 98722d5

Commits on Dec 20, 2023

• ygr 4

  Thmoas-Guan

  committed
  f5f9c11

  Copy full SHA for f5f9c11

• Merge remote-tracking branch 'upstream/master'

  Thmoas-Guan

  committed
  8a78148

  Copy full SHA for 8a78148

• comment of ygr 1 2 4

  Thmoas-Guan

  committed
  64c1b9c

  Copy full SHA for 64c1b9c

Commits on Dec 24, 2023

• refine 1 3 4

  Thmoas-Guan

  committed
  8fb69fd

  Copy full SHA for 8fb69fd

• slight change of ygr 2

  Thmoas-Guan

  committed
  03de22f

  Copy full SHA for 03de22f

• Merge remote-tracking branch 'upstream/master'

  Thmoas-Guan

  committed
  07ffac7

  Copy full SHA for 07ffac7

• Update Basic.lean

  Thmoas-Guan

  committed
  8585ee6

  Copy full SHA for 8585ee6

• 12.24

  Thmoas-Guan

  committed
  dab343b

  Copy full SHA for dab343b

• Merge branch 'pr/6'

  Thmoas-Guan

  committed
  99f5f2d

  Copy full SHA for 99f5f2d

• rw with instance for ygr 1 2 4

  Show description for 59479c0
  Thmoas-Guan

  committed
  59479c0

  Copy full SHA for 59479c0

• refine ygr 1

  Thmoas-Guan

  committed
  93aa6ca

  Copy full SHA for 93aa6ca

• plan about relative side

  Show description for ecd29fd
  Thmoas-Guan

  committed
  ecd29fd

  Copy full SHA for ecd29fd

Commits on Dec 26, 2023

• same side start

  Show description for f0ca549
  Thmoas-Guan

  committed
  f0ca549

  Copy full SHA for f0ca549

Commits on Dec 27, 2023

• define same side

  Thmoas-Guan

  committed
  3db2f69

  Copy full SHA for 3db2f69

• define the true relative side

  Show description for 53be6c3
  Thmoas-Guan

  committed
  53be6c3

  Copy full SHA for 53be6c3

Commits on Dec 28, 2023

• commute of relative side

  Thmoas-Guan

  committed
  06b5924

  Copy full SHA for 06b5924

• trans of same side

  Thmoas-Guan

  committed
  a09810c

  Copy full SHA for a09810c

• anti-trans of Opposite side

  Thmoas-Guan

  committed
  b833e7c

  Copy full SHA for b833e7c

• Update exclusion of left right on

  Thmoas-Guan

  committed
  62ab894

  Copy full SHA for 62ab894

Commits on Dec 29, 2023

• add not colinear

  Show description for b275fbf
  Thmoas-Guan

  committed
  b275fbf

  Copy full SHA for b275fbf

• fix Orientation_trash

  Show description for f962ac8
  Thmoas-Guan

  committed
  f962ac8

  Copy full SHA for f962ac8

• Merge remote-tracking branch 'upstream/master'

  Thmoas-Guan

  committed
  295af97

  Copy full SHA for 295af97

• silly naming problem

  Thmoas-Guan

  committed
  2a4159d

  Copy full SHA for 2a4159d

Commits on Jan 8, 2024

• Refine Proofs at Orientation_trash

  Thmoas-Guan

  committed
  47c5370

  Copy full SHA for 47c5370