[Merged by Bors] - feat: changeLevel for Dirichlet characters

[mo271]

---

[mo271]

@MichaelStollBayreuth adding you here, because of the helpful suggestions in #7010.

[alexjbest]

Can we add some "obvious" lemmas about change level here, like change_level_self for n | n is the identity map, and change_level_trans saying that if n | m | r then changing level twice is the same as changing just once

[mo271]

Can we add some "obvious" lemmas about change level here, like change_level_self for n | n is the identity map, and change_level_trans saying that if n | m | r then changing level twice is the same as changing just once

I was going to do that in a follow-up pull request in order to keep them small, but I'm happy to do it here now. Added those.

[alexjbest]

Can we add some "obvious" lemmas about change level here, like change_level_self for n | n is the identity map, and change_level_trans saying that if n | m | r then changing level twice is the same as changing just once

I was going to do that in a follow-up pull request in order to keep them small, but I'm happy to do it here now. Added those.

I appreciate that! I think there is some sort of happy medium around 100 lines for a new Def + the basic lemmas to be sure that the Def works as intended.

[MichaelStollBayreuth]

Should the indentation in

lemma toUnitHom_eq_char' {a : ZMod n} (ha : IsUnit a) :
  χ a = χ.toUnitHom ha.unit := by simp

lemma toUnitHom_eq_iff (ψ : DirichletCharacter R n) :
  toUnitHom χ = toUnitHom ψ ↔ χ = ψ := by simp

lemma eval_modulus_sub (x : ZMod n) :
  χ (n - x) = χ (-x) := by simp

also be changed (to indent by 4 for statements on the line(s) after ":")?

[mo271]

also be changed (to indent by 4 for statements on the line(s) after ":")?

I just put them on one line.

[MichaelStollBayreuth]

Looks good to me now!

[alexjbest]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by alexjbest.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style