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

Snapshot

fee1907d

chore(data/polynomial/degree): golf a proof

16ddb3a5

Snapshot

163f6f3f

Update src/data/polynomial/degree/definitions.lean

9e283c48

Merge branch 'master' into YK-nat-pos

2b7f6a1d

Merge branch 'YK-unit-nat-pos' into YK-nat-pos

8326a7cd

Snapshot

5ec4f014

Merge branch 'YK-poly-golf' into YK-nat-pos

e62261e3

Merge remote-tracking branch 'origin/YK-poly-golf' into YK-nat-pos

2e8f37b2

Snapshot

2fdd1dc5

Snapshot

3c006ebf

Merge branch 'master' into YK-nat-pos

de10da4b

Remove `#check`

836e38d7

Snapshot

287b1d84

Update

aeca4f44

Fix

0d6cf3fd

Merge branch 'master' into YK-nat-prime-iff

6ba62dc1

Delete lines that were moved to another file

aa45f685

Fix

aa8b47fd

Merge branch 'master' into YK-nat-prime-iff

e9ff9c1b

Fix

801bb59a

Update src/data/nat/prime.lean

7902c3c3

Snapshot

0a5eb9f3

Merge branch 'master' into YK-nat-pos

a34a8208

Merge branch 'YK-nat-prime-iff' into YK-nat-pos

0311694c

Fixes

0915fd09

Merge branch 'master' into YK-nat-pos

31f5239e

Fix

ebfc2b0e

Merge branch 'master' into YK-nat-pos

e20553d0

Merge remote-tracking branch 'origin/YK-nat-prime-iff' into YK-nat-pos

7a6229ae

Fix `norm_num`

062f5e19

Merge branch 'master' into YK-nat-pos

6b5d6ac4

Fix

aab54ee5

Fix

cf49c4d0

Merge branch 'master' into YK-nat-pos

ea9e6465

Fix, golf

9136a289

Snapshot

b6c5c7d3

Fix

fce8eb83

Fix

1deb64fa

Snapshot

fb1dbf72

Merge branch 'master' into YK-nat-pos

ba7dd1c2

Snapshot

d0fae9f0

Update

b685325b

Update

f2ce9e7c

chore(ring_theory/roots_of_unity): golf some proofs

c4b23290

Fix

f0810815

Fix

7f76a42c

Fix

43ca8212

Merge branch 'YK-cyclotomic' into YK-nat-pos

72ae2d26

Merge branch 'master' into YK-prim-roots-golf

8057146c

Merge branch 'YK-prim-roots-golf' into YK-nat-pos

55c4d98a

Merge branch 'master' into YK-nat-pos

161a9af9

Update

5fef9cd9

Update

af5355b5

Fix

fb5fc396

Fix

b0089234

Fix

b1161f4d

Fix, golf

e9a047e1

urkud added t-algebra

urkud added awaiting-review

Merge branch 'master' into YK-nat-pos

377b3122

mathlib-dependent-issues-bot added blocked-by-other-PR

mathlib-dependent-issues-bot removed blocked-by-other-PR

Merge branch 'master' into YK-nat-pos

c90b0eab

feat(ring_theory/integral_domain): generalize `card_fiber_eq_of_mem_r…

9d93764a

mathlib-dependent-issues-bot added blocked-by-other-PR

Golf

87778dbf

Merge branch 'YK-card-fiber-eq' into YK-nat-pos

93ea9628

Merge branch 'master' into YK-nat-pos

ef7162b6

Merge branch 'master' into YK-nat-pos

b473da3e

Revert (moved to another PR)

0697336b

mathlib-dependent-issues-bot removed blocked-by-other-PR

Fix

23acf658

Snapshot

dca0a7ba

Merge branch 'master' into YK-nat-pos

c60c141d

Snapshot

f8e22fa5

Fix

938dcaeb

Fix

1b103e71

Fix

b28f512c

Fix

0fed6e73

Fix

b3ffa025

Merge branch 'YK-nat-log' into YK-nat-pos

527dc71f

Update

46bc0728

Merge branch 'master' into YK-nat-pos

3b30776f

Long line

2e5140ee

Merge branch 'master' into YK-nat-pos

42bf054d

Merge branch 'master' into YK-nat-pos

85d4d748

Fix

c03f8d81

Fix

916c105c

Fix

40c8e8c9

urkud requested a review 3 years ago

Fix

d2d3dc25

Update

a9ed4efc

Fix

01dbd5fb

Snapshot

63ce1f82

Merge branch 'master' into YK-nat-pos

6c7e8ba3

chore(number_theory/padics/padic_val): golf

d27ca25b

Fix

ba3aafcc

Merge branch 'YK-padic-golf' into YK-nat-pos

c3171f48

Update

a3d50553

Snapshot

28b201d9

Fix

1540c061

Fix

d56389a9

Fix

c877e554

YaelDillies added merge-conflict

YaelDillies added awaiting-CI

Fix

2a2831c3

Fix

ee78b0a6

Snapshot

ba975fe0

Update

22590279

Merge branch 'master' into YK-nat-pos

eb06f187

Fix

5a22e4b5

YaelDillies removed merge-conflict

Snapshot

cf4433bd

Merge branch 'master' into YK-nat-pos

015b5649

Merge branch 'master' into YK-nat-pos

dbec302e

Fix

aaa60b75

Cherry-pick

fb25f1b1

Fix

cb13f330

Fix

9ab7e8a6

Golf, use `≠ 0`

7135a584

Fix

d57fa3be

Merge branch 'YK-cycl-eval' into YK-nat-pos

94f97edc

github-actions removed awaiting-CI

...

4e3afee5

Merge branch 'YK-cycl-eval' into YK-nat-pos

9f48a1cb

Fix

4d119346

Golf, fix

4da22d41

Snapshot

73359635

urkud requested a review 3 years ago

urkud removed awaiting-review

urkud added awaiting-author

Fix

e15cf09f

Merge branch 'master' into YK-nat-pos

edf7bbf6

Fix, golf

aae7e91e

Fix

4d22329b

Merge branch 'master' into YK-nat-pos

a4a1bdf5

Fix

6532224d

Fix

9de55954

Fix test

25e44dbc

Merge branch 'master' into YK-nat-pos

d1d66026

Fix

c4ee919b

Merge branch 'master' into YK-nat-pos

9549aa34

Merge branch 'master' into YK-nat-pos

5c8f9278

Snapshot

a68eb726

Merge branch 'master' into YK-cons-divisors

514bf05c

Swap LHS and RHS

a7f46885

Merge branch 'master' into YK-cons-divisors

bd89a386

Merge branch 'YK-cons-divisors' into YK-nat-pos

5eb10e6f

Fix

53583419

mathlib-dependent-issues-bot added blocked-by-other-PR

Merge branch 'master' into YK-nat-pos

dfab0bd7

mathlib-dependent-issues-bot removed blocked-by-other-PR

kim-em added too-late

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

Open

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

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

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

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

Open