PR #1603 feat(data/nat): a lemma about min_fac

feat(data/nat): a lemma about min_fac #1603

mergify merged 10 commits into master from min_fac_le_div

feat(data/nat): a lemma about min_fac

69ccffb1

feat(data/nat): a lemma about min_fac

d9d8a827

kim-em requested a review from

ChrisHughes24 6 years ago

kim-em added awaiting-review

robertylewis commented on 2019-10-24

use Rob's proof

5bf63659

fix

74cbfe22

let's play golf

ac8eb1af

newline

318eb8c6

rwbarton commented on 2019-10-24

ChrisHughes24 commented on 2019-10-24

kim-em removed awaiting-review

kim-em added awaiting-author

use Chris' proof

50090dbb

cleaning up

c7727c86

kim-em removed awaiting-author

kim-em added awaiting-review

ChrisHughes24 commented on 2019-10-25

ChrisHughes24 removed awaiting-review

ChrisHughes24 added awaiting-author

rename per Chris' suggestions

a8e4d3b6

kim-em removed awaiting-author

kim-em added awaiting-review

ChrisHughes24 approved these changes on 2019-10-26

ChrisHughes24 removed awaiting-review

ChrisHughes24 added ready-to-merge

Merge branch 'master' into min_fac_le_div

16575f09

mergify merged b9798dc7 into master 6 years ago

mergify deleted the min_fac_le_div branch 6 years ago

Reviewers

ChrisHughes24

jcommelin

rwbarton

robertylewis

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone

mathlib3 feat(data/nat): a lemma about min_fac #1603 Merged

feat(data/nat): a lemma about min_fac #1603

mathlib3
feat(data/nat): a lemma about min_fac
#1603

Merged