mathlib docs: group_theory.order_of

source

theorem finset.mem_range_iff_mem_finset_range_of_mod_eq {α : Type u_1} [decidable_eq α] {f : ℤ → α} {a : α} {n : ℕ} :

0 < n → (∀ (i : ℤ), f (i % ↑n) = f i) → (a ∈ set.range f ↔ a ∈ finset.image (λ (i : ℕ), f ↑i) (finset.range n))

source

theorem conj_injective {α : Type u_1} [group α] {x : α} :

function.injective (λ (g : α), x * g * x⁻¹)

source

theorem mem_normalizer_fintype {α : Type u_1} [group α] {s : set α} [fintype ↥s] {x : α} :

(∀ (n : α), n ∈ s → x * n * x⁻¹ ∈ s) → x ∈ subgroup.set_normalizer s

source

@[instance]

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

fintype ↥⊥

Equations

fintype_bot = {elems := {1}, complete := _}

source

@[simp]

theorem card_trivial {α : Type u_1} [group α] :

fintype.card ↥⊥ = 1

source

@[instance]

def quotient_group.fintype {α : Type u_1} [group α] [fintype α] (s : subgroup α) [d : decidable_pred (λ (a : α), a ∈ s)] :

fintype (quotient_group.quotient s)

Equations

quotient_group.fintype s = quotient.fintype (quotient_group.left_rel s)

source

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

fintype.card α = fintype.card (quotient_group.quotient s) * fintype.card ↥s

source

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

fintype.card ↥s ∣ fintype.card α

source

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

fintype.card (quotient_group.quotient s) ∣ fintype.card α

source

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

∃ (i : ℤ) (H : i ≠ 0), a ^ i = 1

source

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

∃ (i : ℕ) (H : i > 0), a ^ i = 1

source

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

α → ℕ

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

Equations

order_of a = nat.find _

source

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

a ^ order_of a = 1

source

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

0 < order_of a

source

theorem pow_injective_of_lt_order_of {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] {n m : ℕ} (a : α) :

n < order_of a → m < order_of a → a ^ n = a ^ m → n = m

source

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

order_of a ≤ fintype.card α

source

theorem pow_eq_mod_order_of {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] {n : ℕ} :

a ^ n = a ^ (n % order_of a)

source

theorem gpow_eq_mod_order_of {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] {i : ℤ} :

a ^ i = a ^ (i % ↑(order_of a))

source

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

a' ∈ subgroup.gpowers a ↔ a' ∈ finset.image (has_pow.pow a) (finset.range (order_of a))

source

@[instance]

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

decidable_pred ↑(subgroup.gpowers a)

Equations

decidable_gpowers = λ (a' : α), decidable_of_iff' (a' ∈ finset.image (has_pow.pow a) (finset.range (order_of a))) _

source

theorem order_of_dvd_of_pow_eq_one {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] {n : ℕ} :

a ^ n = 1 → order_of a ∣ n

source

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

source

theorem order_of_le_of_pow_eq_one {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] {n : ℕ} :

0 < n → a ^ n = 1 → order_of a ≤ n

source

theorem sum_card_order_of_eq_card_pow_eq_one {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] {n : ℕ} :

0 < n → (finset.filter (λ (_x : ℕ), _x ∣ n) (finset.range n.succ)).sum (λ (m : ℕ), (finset.filter (λ (a : α), order_of a = m) finset.univ).card) = (finset.filter (λ (a : α), a ^ n = 1) finset.univ).card

source

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

order_of a = fintype.card ↥↑(subgroup.gpowers a)

source

@[simp]

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

order_of 1 = 1

source

@[simp]

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

order_of a = 1 ↔ a = 1

source

theorem order_of_eq_prime {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] {p : ℕ} [hp : fact (nat.prime p)] :

a ^ p = 1 → a ≠ 1 → order_of a = p

source

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

order_of a ∣ fintype.card α

source

@[simp]

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

a ^ fintype.card α = 1

source

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

x ∈ submonoid.powers a ↔ x ∈ subgroup.gpowers a

source

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

↑(submonoid.powers a) = ↑(subgroup.gpowers a)

source

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

source

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

finset.image (λ (i : ℕ), a ^ i) (finset.range (order_of a)) = ↑(subgroup.gpowers a).to_finset

source

theorem pow_gcd_card_eq_one_iff {α : Type u_1} [group α] [fintype α] {n : ℕ} {a : α} :

a ^ n = 1 ↔ a ^ n.gcd (fintype.card α) = 1

source

@[class]

structure is_cyclic (α : Type u_2) [group α] :

Prop

exists_generator : ∃ (g : α), ∀ (x : α), x ∈ subgroup.gpowers g

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

Instances

source

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

comm_group α

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

Equations

is_cyclic.comm_group = {mul := group.mul hg, mul_assoc := _, one := group.one hg, one_mul := _, mul_one := _, inv := group.inv hg, mul_left_inv := _, mul_comm := _}

source

theorem is_cyclic_of_order_of_eq_card {α : Type u_1} [group α] [decidable_eq α] [fintype α] (x : α) :

order_of x = fintype.card α → is_cyclic α

source

theorem order_of_eq_card_of_forall_mem_gpowers {α : Type u_1} [group α] [decidable_eq α] [fintype α] {g : α} :

(∀ (x : α), x ∈ subgroup.gpowers g) → order_of g = fintype.card α

source

@[instance]

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

is_cyclic ↥⊥

Equations

bot.is_cyclic = _

source

@[instance]

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

is_cyclic ↥H

Equations

_ = _
_ = _
_ = _
_ = _
_ = _
_ = _
_ = _
_ = _

source

theorem is_cyclic.card_pow_eq_one_le {α : Type u_1} [group α] [decidable_eq α] [fintype α] [is_cyclic α] {n : ℕ} :

0 < n → (finset.filter (λ (a : α), a ^ n = 1) finset.univ).card ≤ n

source

theorem is_cyclic.exists_monoid_generator (α : Type u_1) [group α] [fintype α] [is_cyclic α] :

∃ (x : α), ∀ (y : α), y ∈ submonoid.powers x

source

theorem is_cyclic.image_range_order_of {α : Type u_1} {a : α} [group α] [decidable_eq α] [fintype α] :

(∀ (x : α), x ∈ subgroup.gpowers a) → finset.image (λ (i : ℕ), a ^ i) (finset.range (order_of a)) = finset.univ

source

theorem is_cyclic.image_range_card {α : Type u_1} {a : α} [group α] [decidable_eq α] [fintype α] :

(∀ (x : α), x ∈ subgroup.gpowers a) → finset.image (λ (i : ℕ), a ^ i) (finset.range (fintype.card α)) = finset.univ

source

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

source

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 : ℕ} :

d ∣ fintype.card α → (finset.filter (λ (a : α), order_of a = d) finset.univ).card = d.totient

source

theorem is_cyclic_of_card_pow_eq_one_le {α : Type u_1} [group α] [decidable_eq α] [fintype α] :

(∀ (n : ℕ), 0 < n → (finset.filter (λ (a : α), a ^ n = 1) finset.univ).card ≤ n) → is_cyclic α

source

theorem is_cyclic.card_order_of_eq_totient {α : Type u_1} [group α] [is_cyclic α] [decidable_eq α] [fintype α] {d : ℕ} :

d ∣ fintype.card α → (finset.filter (λ (a : α), order_of a = d) finset.univ).card = d.totient

mathlib documentation

group_theory.order_of_element

General documentation

Additional documentation

Library

mathlib documentation

group_theory.​order_of_element

General documentation

Additional documentation

Library

group_theory.order_of_element