[Merged by Bors] - feat: small lemmas about moebius #11770
Conversation
Ruben-VandeVelde
commented
Mar 29, 2024
Ruben-VandeVelde
commented
Ruben-VandeVelde
added
the
awaiting-review
|
LGTM maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by loefflerd. |
| @@ -1073,12 +1073,17 @@ theorem moebius_ne_zero_iff_squarefree {n : ℕ} : μ n ≠ 0 ↔ Squarefree n : | |||
| · simp [h, pow_ne_zero] | |||
| #align nat.arithmetic_function.moebius_ne_zero_iff_squarefree ArithmeticFunction.moebius_ne_zero_iff_squarefree | |||
|
|
|||
| theorem moebius_eq_or (n : ℕ) : μ n = 0 ∨ μ n = 1 ∨ μ n = -1 := by | |||
There was a problem hiding this comment.
To me this looks like an argument to change the return type to be SignType
There was a problem hiding this comment.
Wouldn't this just add yet another layer of coercions that you have to translate everything through whenever you want to do arithmetic with μ?
There was a problem hiding this comment.
To push this further, I guess one could argue that ArithmeticFunction.zeta should take values in Fin 2...
There was a problem hiding this comment.
I suspect that the coercions aren't really a problem; and in exchange, you get results like this and the abs one for free
There was a problem hiding this comment.
(if the coercions were really that bad, then presumably SignType wouldn't exist at all!)
There was a problem hiding this comment.
FWIW, I just had a stab at reimplementing μ to be SignType-valued, just to check how bad it would be. It's every bit as bad as I expected. Literally every single lemma in the library about μ would need to be rewritten, with clunkier statements and longer proofs. We'd also need to add a whole load of tedious boilerplate code about coercions ArithmeticFunction SignType → ArithmeticFunction R for appropriate R, and compatibility of these with morphisms between R's. This is really, really not the way to go.
There was a problem hiding this comment.
Thanks for the cross-links. I'll have a think about this some more later, but actually changing this probably isn't a blocker for this PR (I'll let another maintainer decide).
There was a problem hiding this comment.
FWIW, I just had a stab at reimplementing
μto beSignType-valued, just to check how bad it would be
Would you mind sharing the branch with this stab on? No need to PR it, but if you put in the work it's nice to refer back to if this comes up again in future.
|
Thanks for doing this! Once it is in, I'll use it to golf a bit in #11712 as you suggested. |
|
This seems reasonable to me, and I'm not convinced that going to bors merge |
github-actions
bot
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
