[Merged by Bors] - feat(group_theory/perm/cycles): more lemmas

[pechersky]

---

• depends on: [Merged by Bors] - feat(data/finset/noncomm_prod): noncomm_prod_union_of_disjoint #8169

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - feat(data/finset/noncomm_prod): noncomm_prod_union_of_disjoint #8169

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[eric-wieser]

Does this work directly on the lemmas now that to_additive knows about smul and pow? Or is that PR still unmerged?

[pechersky]

After merging master,

type mismatch at application
  @nsmul_injective_of_lt_add_order_of G x
    (n % @add_order_of G (@sub_neg_monoid.to_add_monoid G (@add_group.to_sub_neg_monoid G _inst_1)) x)
term
  n % @add_order_of G (@sub_neg_monoid.to_add_monoid G (@add_group.to_sub_neg_monoid G _inst_1)) x
has type
  ℕ
but is expected to have type
  add_left_cancel_monoid G

So it seems a separate lemma proof is necessary.

[eric-wieser]

@fpvandoorn, any ideas?

[jcommelin]

This is quite a large PR, but what I've seen looks good to me.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests