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

Stream: triage

[Random Issue Bot]

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]

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.