[ refactor ] make n≢i : n ≢ toℕ i argument to lower₁ irrelevant#2783
Closed
jamesmckinna wants to merge 8 commits into
Closed
[ refactor ] make n≢i : n ≢ toℕ i argument to lower₁ irrelevant#2783jamesmckinna wants to merge 8 commits into
n≢i : n ≢ toℕ i argument to lower₁ irrelevant#2783jamesmckinna wants to merge 8 commits into
Commits
Commits on Jul 25, 2025
Commits on Jul 26, 2025
Commits on Jul 27, 2025
- committed