Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

refactor(*): assume ≠0 instead of 0 < _ #17612

Open
wants to merge 137 commits into
base: master
Choose a base branch
from
Open

refactor(*): assume ≠0 instead of 0 < _ #17612

wants to merge 137 commits into from

Conversation

urkud
Copy link
Member

@urkud urkud commented Nov 18, 2022 •
edited by github-actions bot
Loading

urkud added 30 commits November 3, 2022 10:16
@urkud
Snapshot
fee1907
@urkud
chore(data/polynomial/degree): golf a proof
16ddb3a
@urkud
Snapshot
163f6f3
@urkud
Update src/data/polynomial/degree/definitions.lean
9e283c4
@urkud
Merge branch 'master' into YK-nat-pos
2b7f6a1
@urkud
Merge branch 'YK-unit-nat-pos' into YK-nat-pos
8326a7c
@urkud
Snapshot
5ec4f01
@urkud
Merge branch 'YK-poly-golf' into YK-nat-pos
e62261e
@urkud
Merge remote-tracking branch 'origin/YK-poly-golf' into YK-nat-pos
2e8f37b
@urkud
Snapshot
2fdd1dc
@urkud
Snapshot
3c006eb
@urkud
Merge branch 'master' into YK-nat-pos
de10da4
@urkud
Remove #check
836e38d
@urkud
Snapshot
287b1d8
@urkud
Update
aeca4f4
@urkud
Fix
0d6cf3f
@urkud
Merge branch 'master' into YK-nat-prime-iff
6ba62dc
@urkud
Delete lines that were moved to another file
aa45f68
@urkud
Fix
aa8b47f
@urkud
Merge branch 'master' into YK-nat-prime-iff
e9ff9c1
@urkud
Fix
801bb59
@urkud
Update src/data/nat/prime.lean
7902c3c
@urkud
Snapshot
0a5eb9f
@urkud
Merge branch 'master' into YK-nat-pos
a34a820
@urkud
Merge branch 'YK-nat-prime-iff' into YK-nat-pos
0311694
@urkud
Fixes
0915fd0
@urkud
Merge branch 'master' into YK-nat-pos
31f5239
@urkud
Fix
ebfc2b0
@urkud
Merge branch 'master' into YK-nat-pos
e20553d
@urkud
Merge remote-tracking branch 'origin/YK-nat-prime-iff' into YK-nat-pos
7a6229a
@urkud urkud requested a review from a team as a code owner December 30, 2022 09:12
@urkud urkud added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Dec 30, 2022
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jan 17, 2023
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Feb 27, 2023
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@kim-em kim-em added the too-late This PR was ready too late for inclusion in mathlib3 label Jul 16, 2023
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-author A reviewer has asked the author a question or requested changes t-algebra Algebra (groups, rings, fields etc) too-late This PR was ready too late for inclusion in mathlib3
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@urkud @mathlib-dependent-issues-bot @kim-em @YaelDillies