Int.subgroup_cyclic

Stream: mathlib4

[María Inés de Frutos Fernández]

Is there a reason to prefer to state Int.subgroup_cyclic in terms of AddSubgroup.closure instead of using IsAddCyclic?
@Patrick Massot , @Heather Macbeth

[Patrick Massot]

I have no idea what you are talking about. Did I write this?

[María Inés de Frutos Fernández]

You and Heather are listed as the file authors, that is why I pinged you.

[Patrick Massot]

At least I can tell I didn’t know about IsAddCyclic, so that may be the reason

[Yaël Dillies]

Let me blame but I suspect I wrote this

[Patrick Massot]

https://github.com/leanprover-community/mathlib3/pull/4334 I did

[Yaël Dillies]

Indeed it is Heather and you

[Patrick Massot]

And the PR discussion has no mention of is_add_cyclic so I think we simply didn’t notice its existence.

[Patrick Massot]

So feel free to refactor.

[María Inés de Frutos Fernández]

OK, thanks!

[Thomas Browning]

There's no need to have a special lemma for Int since we have the more general: docs#AddSubgroup.isAddCyclic