mathlib documentation

group_theory.order_of_element

theorem finset.mem_range_iff_mem_finset_range_of_mod_eq {α : Type u_1} [decidable_eq α] {f : → α} {a : α} {n : } (hn : 0 < n) (h : ∀ (i : ), f (i % n) = f i) :
a set.range f a finset.image (λ (i : ), f i) (finset.range n)

theorem conj_injective {α : Type u_1} [group α] {x : α} :
function.injective (λ (g : α), (x * g) * x⁻¹)

theorem mem_normalizer_fintype {α : Type u_1} [group α] {s : set α} [fintype s] {x : α} (h : ∀ (n : α), n s(x * n) * x⁻¹ s) :

@[instance]
def fintype_bot {α : Type u_1} [group α] :

Equations
@[simp]
theorem card_trivial {α : Type u_1} [group α] :

theorem card_subgroup_dvd_card {α : Type u_1} [group α] [fintype α] (s : subgroup α) [fintype s] :

theorem card_quotient_dvd_card {α : Type u_1} [group α] [fintype α] (s : subgroup α) [decidable_pred (λ (a : α), a s)] [fintype s] :

theorem exists_gpow_eq_one {α : Type u_1} [group α] [fintype α] (a : α) :
∃ (i : ) (H : i 0), a ^ i = 1

theorem exists_pow_eq_one {α : Type u_1} [group α] [fintype α] (a : α) :
∃ (i : ) (H : i > 0), a ^ i = 1

def order_of {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] (a : α) :

order_of a is the order of the element a, i.e. the n ≥ 1, s.t. a ^ n = 1

Equations
theorem pow_order_of_eq_one {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] (a : α) :
a ^ order_of a = 1

theorem order_of_pos {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] (a : α) :

theorem pow_injective_of_lt_order_of {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] {n m : } (a : α) (hn : n < order_of a) (hm : m < order_of a) (eq : a ^ n = a ^ m) :
n = m

theorem order_of_le_card_univ {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] :

theorem pow_eq_mod_order_of {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] {n : } :
a ^ n = a ^ (n % order_of a)

theorem gpow_eq_mod_order_of {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] {i : } :
a ^ i = a ^ (i % (order_of a))

theorem mem_gpowers_iff_mem_range_order_of {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] {a a' : α} :

@[instance]
def decidable_gpowers {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] :

Equations
theorem order_of_dvd_of_pow_eq_one {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] {n : } (h : a ^ n = 1) :

theorem order_of_dvd_iff_pow_eq_one {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] {n : } :
order_of a n a ^ n = 1

theorem order_of_le_of_pow_eq_one {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] {n : } (hn : 0 < n) (h : a ^ n = 1) :

theorem sum_card_order_of_eq_card_pow_eq_one {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] {n : } (hn : 0 < n) :
∑ (m : ) in finset.filter (λ (_x : ), _x n) (finset.range n.succ), (finset.filter (λ (a : α), order_of a = m) finset.univ).card = (finset.filter (λ (a : α), a ^ n = 1) finset.univ).card

theorem order_eq_card_gpowers {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] :

@[simp]
theorem order_of_one {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] :

@[simp]
theorem order_of_eq_one_iff {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] :
order_of a = 1 a = 1

theorem order_of_eq_prime {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] {p : } [hp : fact (nat.prime p)] (hg : a ^ p = 1) (hg1 : a 1) :

theorem order_of_dvd_card_univ {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] :

@[simp]
theorem pow_card_eq_one {α : Type u_1} [group α] [fintype α] (a : α) :

theorem mem_powers_iff_mem_gpowers {α : Type u_1} [group α] [fintype α] {a x : α} :

theorem powers_eq_gpowers {α : Type u_1} [group α] [fintype α] (a : α) :

theorem order_of_pow {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] (a : α) (n : ) :
order_of (a ^ n) = order_of a / (order_of a).gcd n

theorem image_range_order_of {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] (a : α) :

theorem pow_gcd_card_eq_one_iff {α : Type u_1} [group α] [fintype α] {n : } {a : α} :
a ^ n = 1 a ^ n.gcd (fintype.card α) = 1

@[class]
structure is_cyclic (α : Type u_2) [group α] :
Prop

A group is called cyclic if it is generated by a single element.

Instances
def is_cyclic.comm_group {α : Type u_1} [hg : group α] [is_cyclic α] :

A cyclic group is always commutative. This is not an instance because often we have a better proof of comm_group.

Equations
theorem is_cyclic_of_order_of_eq_card {α : Type u_1} [group α] [decidable_eq α] [fintype α] (x : α) (hx : order_of x = fintype.card α) :

theorem is_cyclic_of_prime_card {α : Type u_1} [group α] [fintype α] {p : } [hp : fact (nat.prime p)] (h : fintype.card α = p) :

theorem order_of_eq_card_of_forall_mem_gpowers {α : Type u_1} [group α] [decidable_eq α] [fintype α] {g : α} (hx : ∀ (x : α), x subgroup.gpowers g) :

@[instance]
def bot.is_cyclic {α : Type u_1} [group α] :

@[instance]
def subgroup.is_cyclic {α : Type u_1} [group α] [is_cyclic α] (H : subgroup α) :

theorem is_cyclic.card_pow_eq_one_le {α : Type u_1} [group α] [decidable_eq α] [fintype α] [is_cyclic α] {n : } (hn0 : 0 < n) :
(finset.filter (λ (a : α), a ^ n = 1) finset.univ).card n

theorem is_cyclic.exists_monoid_generator (α : Type u_1) [group α] [fintype α] [is_cyclic α] :
∃ (x : α), ∀ (y : α), y submonoid.powers x

theorem is_cyclic.image_range_order_of {α : Type u_1} {a : α} [group α] [decidable_eq α] [fintype α] (ha : ∀ (x : α), x subgroup.gpowers a) :

theorem is_cyclic.image_range_card {α : Type u_1} {a : α} [group α] [decidable_eq α] [fintype α] (ha : ∀ (x : α), x subgroup.gpowers a) :

theorem card_pow_eq_one_eq_order_of_aux {α : Type u_1} [group α] [decidable_eq α] [fintype α] (hn : ∀ (n : ), 0 < n(finset.filter (λ (a : α), a ^ n = 1) finset.univ).card n) (a : α) :
(finset.filter (λ (b : α), b ^ order_of a = 1) finset.univ).card = order_of a

theorem card_order_of_eq_totient_aux₂ {α : Type u_1} [group α] [decidable_eq α] [fintype α] (hn : ∀ (n : ), 0 < n(finset.filter (λ (a : α), a ^ n = 1) finset.univ).card n) {d : } (hd : d fintype.card α) :

theorem is_cyclic_of_card_pow_eq_one_le {α : Type u_1} [group α] [decidable_eq α] [fintype α] (hn : ∀ (n : ), 0 < n(finset.filter (λ (a : α), a ^ n = 1) finset.univ).card n) :

theorem is_cyclic.card_order_of_eq_totient {α : Type u_1} [group α] [is_cyclic α] [decidable_eq α] [fintype α] {d : } (hd : d fintype.card α) :