mathlib3
refactor(set_theory/ordinal/cantor_normal_form): CNF as an association list
#16010
Open
Overview
Commits
46
Changes
View On GitHub

refactor(set_theory/ordinal/cantor_normal_form): CNF as an association list #16010

vihdzp wants to merge 46 commits into master from CNF_alist'
vihdzp
vihdzp recursion on alist
d56bc571
vihdzp Update alist.lean
8632f7a3
vihdzp infer args
32c5cf51
vihdzp Update alist.lean
2f8904c9
vihdzp more log lemmas
bd2e94f5
vihdzp reduce scope
592ecdaf
vihdzp do thing
48444cc6
vihdzp Update cantor_normal_form.lean
d31a3229
vihdzp Merge branch 'mod_opow_generalize' into CNF_alist_pre
282ac653
vihdzp Update cantor_normal_form.lean
7d2d31d8
vihdzp Update cantor_normal_form.lean
baae70a3
vihdzp Update cantor_normal_form.lean
d9dbea20
vihdzp Update cantor_normal_form.lean
6edf7e2c
vihdzp Update cantor_normal_form.lean
31aaaa32
vihdzp refactor
3fcb744f
vihdzp Update cantor_normal_form.lean
06467e21
vihdzp Merge branch 'mod_opow_generalize' into CNF_alist_pre
ba843eac
vihdzp Update cantor_normal_form.lean
8cfad10d
vihdzp tweak
e9749159
vihdzp Merge branch 'master' into CNF_alist_pre
6a5b8ae7
vihdzp Merge branch 'master' into CNF_alist_pre
d1f60f99
vihdzp Merge branch 'master' into mod_opow_generalize
1ed83666
vihdzp fix
a415b456
vihdzp Update cantor_normal_form.lean
edf9816e
vihdzp Merge branch 'mod_opow_generalize' into CNF_alist_pre
7e26a48a
vihdzp Merge branch 'master' into CNF_alist_pre
bfe0a9b9
vihdzp start
382ebb5d
vihdzp Merge branch 'alist_recursion' into CNF_alist'
067d8cad
vihdzp finish!
c6ee2612
vihdzp more lemmas on mods
80586b92
vihdzp golf
49512914
vihdzp fix
0ef12a24
vihdzp Merge branch 'master' into CNF_alist'
369bdd51
vihdzp reorder lemmas
8c5dc7a6
vihdzp Update cantor_normal_form.lean
fe358317
vihdzp Merge branch 'more_mod_ord' into CNF_golf
99111f56
vihdzp more golf
68da56d9
vihdzp rename + move
c0151ddd
vihdzp vihdzp added awaiting-review
mathlib-dependent-issues-bot mathlib-dependent-issues-bot added blocked-by-other-PR
vihdzp Merge branch 'master' into CNF_golf
284ff4fa
vihdzp Merge branch 'master' into CNF_golf
ff11e7bf
vihdzp Update src/set_theory/ordinal/cantor_normal_form.lean
545cf6c1
vihdzp Merge branch 'CNF_golf' into CNF_alist'
64d70ca0
vihdzp Merge branch 'master' into CNF_alist'
d6179132
vihdzp Update alist.lean
bb593be6
vihdzp revert simp inlines
7799c309
vihdzp Merge branch 'CNF_golf' into CNF_alist'
10ed7753
vihdzp vihdzp added modifies-synchronized-file
vihdzp vihdzp changed the title feat(set_theory/ordinal/cantor_normal_form): CNF as an association list refactor(set_theory/ordinal/cantor_normal_form): CNF as an association list 2 years ago
mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed blocked-by-other-PR
mathlib-dependent-issues-bot
YaelDillies YaelDillies added merge-conflict
eric-wieser eric-wieser added not-too-late

Login to write a write a comment.

Login via GitHub

Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-review merge-conflict modifies-synchronized-file not-too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum