Zulip Chat Archive
Stream: new members
Topic: lagrange theorem
Leonid Kimelfeld (Jan 22 2019 at 07:58):
Dear all, could you help me. Where is formalization of Lagrange theorem (group theory) in mathlib?
Mario Carneiro (Jan 22 2019 at 08:02):
card_subgroup_dvd_card, I guess? https://github.com/leanprover/mathlib/blob/master/src/group_theory/order_of_element.lean#L56-L58
Mario Carneiro (Jan 22 2019 at 08:02):
there are a few ways you could state the theorem
Leonid Kimelfeld (Jan 22 2019 at 08:08):
card_subgroup_dvd_card, I guess? https://github.com/leanprover/mathlib/blob/master/src/group_theory/order_of_element.lean#L56-L58
Yes, thank you!
Last updated: Dec 20 2023 at 11:08 UTC