Zulip Chat Archive

Stream: triage

Topic: PR #12587: feat(algebra/ring/basic): lemmas about oddness...


Random Issue Bot (Aug 16 2022 at 14:15):

Today I chose PR 12587 for discussion!

feat(algebra/ring/basic): lemmas about oddness of add/sub 1
Created by @damiano (@adomani) on 2022-03-11
Labels: awaiting-author

Is this PR still relevant? Any recent updates? Anyone making progress?

Damiano Testa (Aug 16 2022 at 17:55):

Some of these lemmas are probably obsolete, now that even has been merged with is_square.

Unless someone wants these lemmas, I'll close the PR.


Last updated: Dec 20 2023 at 11:08 UTC