Kevin Buzzard
|
93b980fc79
|
import algorithm world in advanced addition world
|
2024-01-23 20:59:34 +00:00 |
|
Kevin Buzzard
|
396a350bda
|
use mathlib Apply ... At
|
2024-01-23 19:24:42 +00:00 |
|
Kevin Buzzard
|
9e6ce0669e
|
Merge branch 'AdvMultiplication'
|
2024-01-23 18:56:52 +00:00 |
|
Jon Eugster
|
24ac80d224
|
bump to v4.4.0
|
2024-01-12 13:43:29 +01:00 |
|
Kevin Buzzard
|
28b67edb95
|
a note about future worlds
|
2023-12-22 16:44:04 +00:00 |
|
Kevin Buzzard
|
b893d5f1b0
|
remove "if I've written it" comment because I now have
|
2023-12-22 16:36:10 +00:00 |
|
Kevin Buzzard
|
9815f76598
|
hx -> h2 in mul_right_eq_one
|
2023-12-22 16:33:02 +00:00 |
|
Kevin Buzzard
|
ab6b56540d
|
Merge branch 'main' into AdvMultiplication
|
2023-12-22 16:08:12 +00:00 |
|
Kevin Buzzard
|
26a39e3459
|
clarify left and right in three way or
|
2023-12-22 15:55:55 +00:00 |
|
Kevin Buzzard
|
e8ba2a5fee
|
tinkering with text
|
2023-12-22 15:54:43 +00:00 |
|
Kevin Buzzard
|
b8a0fd8c64
|
rename le_of_succ_le_succ to succ_le_succ
|
2023-12-22 15:54:08 +00:00 |
|
Kevin Buzzard
|
4219e68302
|
better LemmaTab for le_succ_self
|
2023-12-22 15:46:10 +00:00 |
|
Kevin Buzzard
|
6f8d7062db
|
delete ne_succ_self level (too hard, never used)
|
2023-12-22 15:36:39 +00:00 |
|
Kevin Buzzard
|
11615ca8fe
|
add sample proofs
|
2023-12-22 15:22:19 +00:00 |
|
Kevin Buzzard
|
58818c9895
|
"Mul" tab -> "*" tab
|
2023-12-22 15:22:09 +00:00 |
|
Kevin Buzzard
|
7b66e800d3
|
add "leave world" explanation
|
2023-12-22 15:00:30 +00:00 |
|
Kevin Buzzard
|
cfe1ae17d5
|
hint for add_succ
|
2023-12-22 14:56:28 +00:00 |
|
Kevin Buzzard
|
9e90d25642
|
0 -> $0$ in tutorial
|
2023-12-22 14:54:25 +00:00 |
|
Kevin Buzzard
|
dc0dd30736
|
tidying up
|
2023-12-22 14:18:03 +00:00 |
|
Kevin Buzzard
|
caf6e47ec8
|
hopefully finished advanced multiplication world!
|
2023-12-21 22:09:02 +00:00 |
|
Kevin Buzzard
|
b81f2ecced
|
Advanced multiplication minor reorganisation
|
2023-12-21 17:12:40 +00:00 |
|
Kevin Buzzard
|
633b39d65a
|
add statememt name and lemmadoc
|
2023-12-21 17:12:18 +00:00 |
|
Kevin Buzzard
|
693051fc84
|
Merge branch 'main' into AdvMultiplication
|
2023-12-20 14:17:43 +00:00 |
|
Kevin Buzzard
|
70104f2018
|
tinkering with docs in advanced + world
|
2023-12-20 14:15:21 +00:00 |
|
Kevin Buzzard
|
16e544acb5
|
add le_one and le_two to <= levels
|
2023-12-20 14:06:14 +00:00 |
|
Kevin Buzzard
|
c29085799e
|
rename eq_zero_of_add_left/right_eq_zero to just add_left/right_eq_zero
|
2023-12-20 14:05:48 +00:00 |
|
Kevin Buzzard
|
318a3a0b2c
|
delete dead code
|
2023-12-20 13:53:08 +00:00 |
|
Kevin Buzzard
|
9a2cc07563
|
rewording to prepare for more advanced addition levels
|
2023-12-20 13:52:53 +00:00 |
|
Kevin Buzzard
|
98598bffa1
|
oh I'm a fool, original lemmatab was better
|
2023-12-20 13:39:29 +00:00 |
|
Kevin Buzzard
|
09c16e9f2a
|
more appropriate lemma tab for implication L10
|
2023-12-20 13:37:34 +00:00 |
|
Kevin Buzzard
|
ce975ae46b
|
fix typo in inequality level 4
|
2023-12-20 13:30:43 +00:00 |
|
Kevin Buzzard
|
72364d6c1c
|
more minor tinkering with wording in algo world
|
2023-12-19 16:27:17 +00:00 |
|
Kevin Buzzard
|
bba9ed4521
|
more succ_ne_zero tinkering
|
2023-12-19 15:59:38 +00:00 |
|
Kevin Buzzard
|
b7a7beeee1
|
better triv tactic doc
|
2023-12-19 15:54:19 +00:00 |
|
Kevin Buzzard
|
3ee3082667
|
use cases instead of tauto (so we can introduce tauto elsewhere)
|
2023-12-18 17:51:19 +00:00 |
|
Kevin Buzzard
|
1f00de56fb
|
delete gitpod file as not relevant here
|
2023-12-18 16:40:24 +00:00 |
|
Kevin Buzzard
|
9c2c7b3b70
|
Better conclusion to => world
|
2023-12-18 16:39:21 +00:00 |
|
Kevin Buzzard
|
421db4c504
|
grammar tinkering
|
2023-12-18 16:39:04 +00:00 |
|
Kevin Buzzard
|
afa3bc7b04
|
start impl levels 9,10 on numerals tab
|
2023-12-18 16:27:33 +00:00 |
|
Kevin Buzzard
|
c13ec0efe0
|
add hint for 1 != 0
|
2023-12-18 16:23:21 +00:00 |
|
Kevin Buzzard
|
cb287aaa54
|
typos in impl world level 10
|
2023-12-18 16:22:17 +00:00 |
|
Kevin Buzzard
|
e47884d92c
|
add docstring for !=
|
2023-12-18 16:15:52 +00:00 |
|
Kevin Buzzard
|
4d142ffaac
|
add docstring for <=
|
2023-12-18 16:15:41 +00:00 |
|
Kevin Buzzard
|
0e7a8d4ca2
|
clarify which goal we're talking about
|
2023-12-18 15:52:42 +00:00 |
|
Kevin Buzzard
|
5fc27502ec
|
clarify what to do after finishing + world
|
2023-12-18 15:50:09 +00:00 |
|
Kevin Buzzard
|
d6ba30f71b
|
clarification of rw
|
2023-12-18 15:41:38 +00:00 |
|
Kevin Buzzard
|
4cc1415707
|
fix ref to theorem tabs
|
2023-12-18 15:32:14 +00:00 |
|
Jon Eugster
|
f4028d7a05
|
Add definitions Ne and LE
|
2023-12-15 15:50:45 +01:00 |
|
Jon Eugster
|
a71cd97373
|
fix pretty-printing of Power. #46
|
2023-12-15 15:22:45 +01:00 |
|
Jon Eugster
|
a126620f31
|
update workflow to build gameserver
|
2023-12-08 18:52:53 +01:00 |
|