Re: [isabelle] Weak lemma: HOL-Algebra.Multiplicative_Group.generate_pow_card

[Florian Haftmann <florian.haftmann at 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

Am 13.11.20 um 19:34 schrieb Jakub Kądziołka:
> On Fri Nov 13, 2020 at 7:25 PM CET, Jakub Kądziołka wrote:
>> Greetings,
>>
>> currently, generate_pow_card assumes "finite (carrier G)". This is
>> unnecessary, as evidenced by the modified proof I'm including below.
>> I modified two lemmas above it to only assume that a relevant subgroup
>> is finite, instead of the entire group. Also, the removed assumption
>> leads to a simpler proof of ord_dvd_group_order.
>>
>> Regards,
>> 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
> 
> Regards,
> Jakub Kądziołka
>

Attachment: signature.asc
Description: OpenPGP digital signature