Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Weak lemma: HOL-Algebra.Multiplicative_Group.g...

view this post on Zulip Email Gateway (Nov 13 2020 at 18:36):

From: Jakub Kądziołka <>
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

Jakub Kądziołka

view this post on Zulip Email Gateway (Feb 25 2021 at 16:50):

From: Florian Haftmann <>
Hi Jakub,

I am not sure whether this thread has been concluded already.

Your contributions are part of the Isabelle2021 release.


Last updated: Jul 15 2022 at 23:21 UTC