8000 Commits · jakelev/lean-rsk · GitHub

More Web Proxy on the site http://driver.im/

Commits

Commits on Aug 3, 2022

update to documentation
jakelev
committed

Commits on Aug 2, 2022

rectangle shapes
jakelev
committed

Commits on May 14, 2022

wip (finished definition of one step of inverse row bumping)
jakelev
committed

Commits on May 13, 2022

wip (started defining inverse row insertion)
jakelev
committed

Commits on May 12, 2022

added docstring
jakelev
committed
wip (some cleanup now that the forward direction of RSK is fully defined)

Jake Levinson
authored and
jakelev
committed

Commits on May 11, 2022

finished the definition of row insertion (forward direction of RSK)

Jake Levinson
authored and
Jake Levinson
committed

Commits on May 10, 2022

wip (defined recording tableau, mostly defined forward direction of rsk)

Jake Levinson
authored and
Jake Levinson
committed

Commits on May 9, 2022

wip (improved proof of ssyt.rbs_cert.rbwf_pieri, started work on recording tableau)

Jake Levinson
authored and
Jake Levinson
committed

Commits on May 8, 2022

wip (finished a longish proof of lemma ssyt.rbs_cert.rbwf_pieri)

Jake Levinson
authored and
Jake Levinson
committed

Commits on May 7, 2022

wip (continued the hard proof of lemma ssyt.rbs_cert.rbwf_pieri)

Jake Levinson
authored and
Jake Levinson
committed

Commits on May 4, 2022

wip (added one step of row insertion)

Jake Levinson
authored and
Jake Levinson
committed

Commits on May 1, 2022

wip (mostly finished young_diagram.lean and ssyt.lean)

Jake Levinson
authored and
Jake Levinson
committed

Commits on Apr 27, 2022

wip rsk: added def of ssyt and fintype instance for bounded ssyts

Jake Levinson
authored and
Jake Levinson
committed

Commits on Apr 25, 2022

first commit (definition of young diagram)

Jake Levinson
authored and
Jake Levinson
committed

0