Grace/Cumulus/Algebra/Group/GroupOrder.g17

Imports

Declarations

elementOrder.divides_order theorem derivation
elementOrder.le_order theorem derivation
pow_order_eq_one theorem derivation

Source

1-- The order of a finite group against its elements: the order of an2-- element divides the order of the group and is at most it, and the order3-- of the group annihilates every element4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Algebra.Group.GroupOrder10import ElementOrder1112section GroupOrder13variable (G : Set)14hypothesis group : Group(G)1516theorem elementOrder.divides_order (g : G)17  requires finite : Finite(G)18  shows elementOrder(G, g) ∣ order(G)19proof20  rw order.value21  exact elementOrder.dvd_card with *2223theorem elementOrder.le_order (g : G)24  requires finite : Finite(G)25  shows elementOrder(G, g) ≤ order(G)26proof27  rw order.value28  exact elementOrder.le_card with *2930theorem pow_order_eq_one (g : G)31  requires finite : Finite(G)32  shows g ^ order(G) = G.one33proof34  rw order.value35  exact Group.pow_card with *3637end GroupOrder38