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

Commits
  • feat(number_theory/divisors): redefine nat.divisors as a monoid hom
    b-mehta committed 3 years ago
  • add docstring for divisors
    b-mehta committed 3 years ago
  • more wip
    b-mehta committed 3 years ago
  • more wip
    b-mehta committed 3 years ago
  • caches pls
    b-mehta committed 3 years ago
  • cleanup
    b-mehta committed 3 years ago
  • fix build
    b-mehta committed 3 years ago
  • Merge branch 'master' into divisors-monoid-hom
    eric-wieser committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into divisors-monoid-hom
    eric-wieser committed 3 years ago
  • Update src/number_theory/divisors.lean
    eric-wieser committed 3 years ago
Loading