How to answer to this beginner question?

Stream: general

[Riccardo Brasca]

I guess we all have seen several times the question "How do we prove that $H \subseteq G$ is a group?" or a variant.

Is someone willing to write a precise answer once and for all that we can quote every time this kind of questions is asked? I think it is a very natural question for a beginner, and understanding that we bundle data is not that easy at the beginning.

I don't have time to do it (and I don't think my answer would be very good), but it would very nice if someone else volunteers.

[Patrick Massot]

There are explanations at https://leanprover-community.github.io/mathematics_in_lean/C07_Hierarchies.html#sub-objects, but they may assume too much knowledge of Lean if this is the first question someone asks.

[Riccardo Brasca]

Yes, of course it is explained in MIL, and several times on Zulip. The problem is that a lot of beginners think they'll will find something like "the even numbers are a subgroup because 0 is even and the set is stable under subtraction". Then they're surprised that the statement is not in mathlib, and even more surprised when we explain that we don't want to formulate the statement like this.

[Yury G. Kudryashov]

Do we have "the set of numbers divisible by a is a subgroup"?

[Yury G. Kudryashov]

Also, we can have a constructor Subgroup.ofDivMem (if we don't have it yet). Is there something wrong with it?

[Ruben Van de Velde]

Something like docs#AddSubgroup.zmultiples or something else?

[Yury G. Kudryashov]

Or as the principal ideal (interpreted as an additive subgroup).

[Yury G. Kudryashov]

Of ocurse, they're the same for Int.