mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: No wrap-around principle for 3APs

Open YaelDillies opened this issue 1 year ago • 1 comments
trafficstars

Prove that {0, ..., k - 1} ⊆ ℤ/(n + 1)ℤ and {0, ..., k - 1} ⊆ ℕ are m-Freiman isomorphic if m * k ≤ n

  • [x] depends on: #12542
  • [x] depends on: #12546

Open in Gitpod

YaelDillies avatar Apr 30 '24 13:04 YaelDillies

This PR/issue depends on:

  • ~~leanprover-community/mathlib4#12542~~
  • ~~leanprover-community/mathlib4#12546~~ By Dependent Issues (🤖). Happy coding!

leanprover-community-mathlib4-bot avatar May 08 '24 10:05 leanprover-community-mathlib4-bot

Thanks :tada:

bors merge

jcommelin avatar May 28 '24 11:05 jcommelin

Pull request successfully merged into master.

Build succeeded:

mathlib-bors[bot] avatar May 28 '24 12:05 mathlib-bors[bot]