Re: [isabelle] Weak lemma: HOL-Algebra.Multiplicative_Group.generate_pow_card
- To: Jakub Kądziołka <kuba at kadziolka.net>, cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Weak lemma: HOL-Algebra.Multiplicative_Group.generate_pow_card
- From: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>
- Date: Thu, 25 Feb 2021 17:50:12 +0100
- Autocrypt: addr=florian.haftmann at informatik.tu-muenchen.de; keydata= mDMEW4pH0BYJKwYBBAHaRw8BAQdAIIBLFhTF7RSAZredeYMftpgRJZSF5X3VVtso084X3660 PUZsb3JpYW4gSGFmdG1hbm4gPGZsb3JpYW4uaGFmdG1hbm5AaW5mb3JtYXRpay50dS1tdWVu Y2hlbi5kZT6IlgQTFggAPgIbAwULCQgHAgYVCgkICwIEFgIDAQIeAQIXgBYhBILJqbJrurlT 4Zn85KcHFyIyz6TpBQJf7KrvBQkGZIwfAAoJEKcHFyIyz6Tp/ugBAL2yRfjY1/2YxFcedOFp bRJFZ7H7SGVL0UeX9hLNOanwAP9PCZrz644aWsVleb52yi/CL0K8Q/WfXLH76xhpYGQLCrg4 BFuKR9ASCisGAQQBl1UBBQEBB0CU8ZQJlBvMpEyGnR4jpUF+HavpBguEs4uAxFQBY21SHgMB CAeIfgQYFggAJgIbDBYhBILJqbJrurlT4Zn85KcHFyIyz6TpBQJf7Kt0BQkGZIykAAoJEKcH FyIyz6TpTTYA/0ysxqOA8YYInFnDdp+ZoLM0Djahh4MUyQ3OCpz6U4/kAP9MfgQqCyGJskPe nGsCTrHdcW760UZ3KMge7vAVPw1eD7gzBFuKSn4WCSsGAQQB2kcPAQEHQNf9JkHWQaDR5cRm q0x7ltlUFok5Z8rfCtOZxVITGGyWiPUEGBYIACYCGwIWIQSCyamya7q5U+GZ/OSnBxciMs+k 6QUCX+yrdAUJBmSJ9gCBdiAEGRYIAB0WIQQ2aRv8hQWta5iN4IfgIQ1PG8W1PgUCW4pKfgAK CRDgIQ1PG8W1PnBCAQDX4Yp8i5GA7fZR8gysMIvUEqnewxPv5MVUrzjSxyNM9gEAvShATZq0 bLwrDJXiPvB+8WLvG9SXWgMLbvt8iSJ2wwwJEKcHFyIyz6TpAj4BAPFUzBamR3bW2iTA/s8r WX4sadNSMoD2Cem5PKQ07YzRAPwNdh4EF4XWcmAzHFyei2sp/KFUgNsgJQ8/iKAcDCRxCg==
- In-reply-to: <C72COIFU170E.XKEK6MHPZXB4@gravity>
- References: <C72COIFU170E.XKEK6MHPZXB4@gravity>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.10.0
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.