Zulip Chat Archive

Stream: new members

Topic: Something about how to use theorem

Move fast (Apr 12 2025 at 05:42):

image.png
How can I solve this problem? About the direct product of subgroups in "theorem" type.

Notification Bot (Apr 12 2025 at 05:45):

A message was moved here from #mathlib4 > Placing a definition in DedekindDomain.Ideal by Move fast.

Ruben Van de Velde (Apr 12 2025 at 06:24):

Please share a #mwe

Notification Bot (Apr 12 2025 at 06:35):

This topic was moved here from #mathlib4 > Something about how to use theorem by Yury G. Kudryashov.

Yury G. Kudryashov (Apr 12 2025 at 06:36):

@Move fast I moved your message to a more appropriate channel.

Move fast (Apr 12 2025 at 06:39):

(deleted)

Yury G. Kudryashov (Apr 12 2025 at 06:40):

Besides sharing a #mwe, please answer some questions:

  • what's your experience with (a) math; (b) lean?
  • why are you interested in this particular question?
  • what informal proof are you going to follow?

Move fast (Apr 12 2025 at 06:42):

(deleted)

Last updated: May 02 2025 at 03:31 UTC