Skip to content

refactor: appeal to `Sum` elimination, rather than `with`

fd375b6
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
Open

[ add ] injectivity of suc for relation m ≡ n (mod o) for {{NonZero o}} #2971

refactor: appeal to `Sum` elimination, rather than `with`
fd375b6
Select commit
Loading
Failed to load commit list.

Annotations

1 warning
check-whitespace
succeeded Apr 2, 2026 in 7s