New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

shorten proofs #4569

Merged

wlammen merged 2 commits into metamath:develop from wlammen:wl-r

Jan 13, 2025

Contributor

wlammen commented Jan 13, 2025

rabeqcda: The new proof makes better use of the pool of variants of similar theorems, but is essentially the same. So I consider it a minimization not in need of an OLD version
rabeqbidv: At the time the old proof was created, rabeqbidva did not exist. So this is a minimization again.
Delete outdated OLD proofs.
Fix a link in rabbi.

wlammen added 2 commits

January 13, 2025 10:19


          shorten rabeqcda

6e4e013


          shorten rabeqbidv

5d766a0

benjub approved these changes

View reviewed changes

icecream17 approved these changes

View reviewed changes

wlammen merged commit 9832dbb into metamath:develop

10 checks passed

wlammen deleted the wl-r branch

January 13, 2025 16:59

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet