mathlib3
refactor(number_theory/divisors): redefine nat.divisors as a monoid hom
#16917

Open

refactor(number_theory/divisors): redefine nat.divisors as a monoid hom #16917

b-mehta wants to merge 10 commits into master from divisors-monoid-hom

feat(number_theory/divisors): redefine nat.divisors as a monoid hom

49fc7880

b-mehta added WIP

b-mehta added awaiting-CI

add docstring for divisors

15ea44de

more wip

95d3d612

more wip

b66a819e

caches pls

e5980b2e

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

cleanup

f0034709

b-mehta removed WIP

b-mehta added awaiting-review

b-mehta changed the title ~~feat(number_theory/divisors): redefine nat.divisors as a monoid hom~~ refactor(number_theory/divisors): redefine nat.divisors as a monoid hom 3 years ago

fix build

8785fbbf

eric-wieser commented on 2022-10-19

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

Merge branch 'master' into divisors-monoid-hom

7bca4039

eric-wieser force pushed from 9eba3437 to 7bca4039 3 years ago

Vierkantor assigned

Vierkantor 3 years ago

Vierkantor commented on 2022-11-02

Vierkantor removed awaiting-review

Vierkantor added awaiting-author

Merge remote-tracking branch 'origin/master' into divisors-monoid-hom

8845358f

Update src/number_theory/divisors.lean

b5bbf010

kim-em added too-late

Reviewers

Vierkantor

eric-wieser

Assignees

Vierkantor

Labels

awaiting-author awaiting-CI too-late

Milestone

No milestone

mathlib3 refactor(number_theory/divisors): redefine nat.divisors as a monoid hom #16917 Open

refactor(number_theory/divisors): redefine nat.divisors as a monoid hom #16917

mathlib3
refactor(number_theory/divisors): redefine nat.divisors as a monoid hom
#16917

Open