p-groups #
This file contains a proof that if G
is a p
-group acting on a finite set α
,
then the number of fixed points of the action is congruent mod p
to the cardinality of α
.
It also contains proofs of some corollaries of this lemma about existence of fixed points.
If gcd(p,n) = 1
, then the n
th power map is a bijection.
Equations
- hG.powEquiv hn = { toFun := fun (x : G) => x ^ n, invFun := fun (g : G) => ↑((powCoprime ⋯).symm ⟨g, ⋯⟩), left_inv := ⋯, right_inv := ⋯ }
Instances For
If a p-group acts on α
and the cardinality of α
is not a multiple
of p
then the action has a fixed point.
If a p-group acts on α
and the cardinality of α
is a multiple
of p
, and the action has one fixed point, then it has another fixed point.
finite p-groups with different p have coprime orders
p-groups with different p are disjoint
A group of order p ^ 2
is commutative. See also IsPGroup.commutative_of_card_eq_prime_sq
for just the proof that ∀ a b, a * b = b * a