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 <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

view this post on Zulip 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: Oct 25 2021 at 20:20 UTC