Email Gateway (Nov 13 2020 at 18:36): Email Gateway (Nov 13 2020 at 18:36):From: Jakub Kądziołka <kuba@kadziolka.net>
I would also like to suggest the following alternative statement of the
lemma, as I believe it would be easier to find with find_theorems in
some situations:
lemma (in group) cyclic_order_is_ord:
assumes "g ∈ carrier G"
shows "ord g = order (subgroup_generated G {g})"
unfolding order_def subgroup_generated_def
using assms generate_pow_card by simp
Regards,
Jakub Kądziołka
Email Gateway (Feb 25 2021 at 16:50):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Jakub,
I am not sure whether this thread has been concluded already.
Your contributions are part of the Isabelle2021 release.
Cheers,
Florian
signature.asc
Last updated: Jan 04 2025 at 20:18 UTC