Exponent of a group

This file defines the exponent of a group, or more generally a monoid. For a group G it is defined to be the minimal n≥1 such that g ^ n = 1 for all g ∈ G. For a finite group G, it is equal to the lowest common multiple of the order of all elements of the group G.

Main definitions

• Monoid.ExponentExists is a predicate on a monoid G saying that there is some positive n such that g ^ n = 1 for all g ∈ G.
• Monoid.exponent defines the exponent of a monoid G as the minimal positive n such that g ^ n = 1 for all g ∈ G, by convention it is 0 if no such n exists.
• AddMonoid.ExponentExists the additive version of Monoid.ExponentExists.
• AddMonoid.exponent the additive version of Monoid.exponent.

Main results

• Monoid.lcm_order_eq_exponent: For a finite left cancel monoid G, the exponent is equal to the Finset.lcm of the order of its elements.
• Monoid.exponent_eq_iSup_orderOf('): For a commutative cancel monoid, the exponent is equal to ⨆ g : G, orderOf g (or zero if it has any order-zero elements).
• Monoid.exponent_pi and Monoid.exponent_prod: The exponent of a finite product of monoids is the least common multiple (Finset.lcm and lcm, respectively) of the exponents of the constituent monoids.
• MonoidHom.exponent_dvd: If f : M₁ →⋆ M₂ is surjective, then the exponent of M₂ divides the exponent of M₁.

TODO

• Refactor the characteristic of a ring to be the exponent of its underlying additive group.

def Monoid.ExponentExists (G : Type u) [Monoid G] : Prop

A predicate on a monoid saying that there is a positive integer n such that g ^ n = 1 for all g.

Equations

• Monoid.ExponentExists G = ∃ (n : ℕ), 0 < n ∧ ∀ (g : G), g ^ n = 1

def AddMonoid.ExponentExists (G : Type u) [AddMonoid G] : Prop

A predicate on an additive monoid saying that there is a positive integer n such

that n • g = 0 for all g.

Equations

• AddMonoid.ExponentExists G = ∃ (n : ℕ), 0 < n ∧ ∀ (g : G), n • g = 0

noncomputable def Monoid.exponent (G : Type u) [Monoid G] : ℕ

The exponent of a group is the smallest positive integer n such that g ^ n = 1 for all g ∈ G if it exists, otherwise it is zero by convention.

Equations

• Monoid.exponent G = if h : Monoid.ExponentExists G then Nat.find h else 0

noncomputable def AddMonoid.exponent (G : Type u) [AddMonoid G] : ℕ

The exponent of an additive group is the smallest positive integer n such that

n • g = 0 for all g ∈ G if it exists, otherwise it is zero by convention.

Equations

• AddMonoid.exponent G = if h : AddMonoid.ExponentExists G then Nat.find h else 0

@[simp]

theorem AddMonoid.exponent_additive {G : Type u} [Monoid G] : exponent (Additive G) = Monoid.exponent G

@[simp]

theorem Monoid.exponent_multiplicative {G : Type u_1} [AddMonoid G] : exponent (Multiplicative G) = AddMonoid.exponent G

@[simp]

theorem MulOpposite.exponent {G : Type u} [Monoid G] : Monoid.exponent Gᵐᵒᵖ = Monoid.exponent G

@[simp]

theorem AddOpposite.exponent {G : Type u} [AddMonoid G] : AddMonoid.exponent Gᵃᵒᵖ = AddMonoid.exponent G

theorem Monoid.ExponentExists.isOfFinOrder {G : Type u} [Monoid G] (h : ExponentExists G) {g : G} : IsOfFinOrder g

theorem AddMonoid.ExponentExists.isOfFinAddOrder {G : Type u} [AddMonoid G] (h : ExponentExists G) {g : G} : IsOfFinAddOrder g

theorem Monoid.ExponentExists.orderOf_pos {G : Type u} [Monoid G] (h : ExponentExists G) (g : G) : 0 < orderOf g

theorem AddMonoid.ExponentExists.addOrderOf_pos {G : Type u} [AddMonoid G] (h : ExponentExists G) (g : G) : 0 < addOrderOf g

theorem Monoid.exponent_ne_zero {G : Type u} [Monoid G] : exponent G ≠ 0 ↔ ExponentExists G

theorem AddMonoid.exponent_ne_zero {G : Type u} [AddMonoid G] : exponent G ≠ 0 ↔ ExponentExists G

theorem Monoid.ExponentExists.exponent_ne_zero {G : Type u} [Monoid G] : ExponentExists G → exponent G ≠ 0

Alias of the reverse direction of Monoid.exponent_ne_zero.

theorem AddMonoid.ExponentExists.exponent_ne_zero {G : Type u} [AddMonoid G] : ExponentExists G → exponent G ≠ 0

theorem Monoid.exponent_pos {G : Type u} [Monoid G] : 0 < exponent G ↔ ExponentExists G

theorem AddMonoid.exponent_pos {G : Type u} [AddMonoid G] : 0 < exponent G ↔ ExponentExists G

theorem Monoid.ExponentExists.exponent_pos {G : Type u} [Monoid G] : ExponentExists G → 0 < exponent G

Alias of the reverse direction of Monoid.exponent_pos.

theorem AddMonoid.ExponentExists.exponent_pos {G : Type u} [AddMonoid G] : ExponentExists G → 0 < exponent G

theorem Monoid.exponent_eq_zero_iff {G : Type u} [Monoid G] : exponent G = 0 ↔ ¬ExponentExists G

theorem AddMonoid.exponent_eq_zero_iff {G : Type u} [AddMonoid G] : exponent G = 0 ↔ ¬ExponentExists G

theorem Monoid.exponent_eq_zero_of_order_zero {G : Type u} [Monoid G] {g : G} (hg : orderOf g = 0) : exponent G = 0

theorem AddMonoid.exponent_eq_zero_addOrder_zero {G : Type u} [AddMonoid G] {g : G} (hg : addOrderOf g = 0) : exponent G = 0

theorem Monoid.exponent_eq_zero_iff_forall {G : Type u} [Monoid G] : exponent G = 0 ↔ ∀ n > 0, ∃ (g : G), g ^ n ≠ 1

The exponent is zero iff for all nonzero n, one can find a g such that g ^ n ≠ 1.

theorem AddMonoid.exponent_eq_zero_iff_forall {G : Type u} [AddMonoid G] : exponent G = 0 ↔ ∀ n > 0, ∃ (g : G), n • g ≠ 0

The exponent is zero iff for all nonzero n, one can find a g such that n • g ≠ 0.

theorem Monoid.pow_exponent_eq_one {G : Type u} [Monoid G] (g : G) : g ^ exponent G = 1

theorem AddMonoid.exponent_nsmul_eq_zero {G : Type u} [AddMonoid G] (g : G) : exponent G • g = 0

theorem Monoid.pow_eq_mod_exponent {G : Type u} [Monoid G] {n : ℕ} (g : G) : g ^ n = g ^ (n % exponent G)

theorem AddMonoid.nsmul_eq_mod_exponent {G : Type u} [AddMonoid G] {n : ℕ} (g : G) : n • g = (n % exponent G) • g

theorem Monoid.exponent_pos_of_exists {G : Type u} [Monoid G] (n : ℕ) (hpos : 0 < n) (hG : ∀ (g : G), g ^ n = 1) : 0 < exponent G

theorem AddMonoid.exponent_pos_of_exists {G : Type u} [AddMonoid G] (n : ℕ) (hpos : 0 < n) (hG : ∀ (g : G), n • g = 0) : 0 < exponent G

theorem Monoid.exponent_min' {G : Type u} [Monoid G] (n : ℕ) (hpos : 0 < n) (hG : ∀ (g : G), g ^ n = 1) : exponent G ≤ n

theorem AddMonoid.exponent_min' {G : Type u} [AddMonoid G] (n : ℕ) (hpos : 0 < n) (hG : ∀ (g : G), n • g = 0) : exponent G ≤ n

theorem Monoid.exponent_min {G : Type u} [Monoid G] (m : ℕ) (hpos : 0 < m) (hm : m < exponent G) : ∃ (g : G), g ^ m ≠ 1

theorem AddMonoid.exponent_min {G : Type u} [AddMonoid G] (m : ℕ) (hpos : 0 < m) (hm : m < exponent G) : ∃ (g : G), m • g ≠ 0

theorem Monoid.exp_eq_one_iff {G : Type u} [Monoid G] : exponent G = 1 ↔ Subsingleton G

theorem AddMonoid.exp_eq_one_iff {G : Type u} [AddMonoid G] : exponent G = 1 ↔ Subsingleton G

@[simp]

theorem Monoid.exp_eq_one_of_subsingleton {G : Type u} [Monoid G] [hs : Subsingleton G] : exponent G = 1

@[simp]

theorem AddMonoid.exp_eq_one_of_subsingleton {G : Type u} [AddMonoid G] [hs : Subsingleton G] : exponent G = 1

theorem Monoid.order_dvd_exponent {G : Type u} [Monoid G] (g : G) : orderOf g ∣ exponent G

theorem AddMonoid.addOrder_dvd_exponent {G : Type u} [AddMonoid G] (g : G) : addOrderOf g ∣ exponent G

theorem Monoid.orderOf_le_exponent {G : Type u} [Monoid G] (h : ExponentExists G) (g : G) : orderOf g ≤ exponent G

theorem AddMonoid.addOrderOf_le_exponent {G : Type u} [AddMonoid G] (h : ExponentExists G) (g : G) : addOrderOf g ≤ exponent G

theorem Monoid.exponent_dvd_iff_forall_pow_eq_one {G : Type u} [Monoid G] {n : ℕ} : exponent G ∣ n ↔ ∀ (g : G), g ^ n = 1

theorem AddMonoid.exponent_dvd_iff_forall_nsmul_eq_zero {G : Type u} [AddMonoid G] {n : ℕ} : exponent G ∣ n ↔ ∀ (g : G), n • g = 0

theorem Monoid.exponent_dvd_of_forall_pow_eq_one {G : Type u} [Monoid G] {n : ℕ} : (∀ (g : G), g ^ n = 1) → exponent G ∣ n

Alias of the reverse direction of Monoid.exponent_dvd_iff_forall_pow_eq_one.

theorem AddMonoid.exponent_dvd_of_forall_nsmul_eq_zero {G : Type u} [AddMonoid G] {n : ℕ} : (∀ (g : G), n • g = 0) → exponent G ∣ n

theorem Monoid.exponent_dvd {G : Type u} [Monoid G] {n : ℕ} : exponent G ∣ n ↔ ∀ (g : G), orderOf g ∣ n

theorem AddMonoid.exponent_dvd {G : Type u} [AddMonoid G] {n : ℕ} : exponent G ∣ n ↔ ∀ (g : G), addOrderOf g ∣ n

theorem Monoid.lcm_orderOf_dvd_exponent (G : Type u) [Monoid G] [Fintype G] : Finset.univ.lcm orderOf ∣ exponent G

theorem AddMonoid.lcm_addOrderOf_dvd_exponent (G : Type u) [AddMonoid G] [Fintype G] : Finset.univ.lcm addOrderOf ∣ exponent G

theorem Nat.Prime.exists_orderOf_eq_pow_factorization_exponent (G : Type u) [Monoid G] {p : ℕ} (hp : Prime p) : ∃ (g : G), orderOf g = p ^ (Monoid.exponent G).factorization p

theorem Nat.Prime.exists_addOrderOf_eq_pow_padic_val_nat_add_exponent (G : Type u) [AddMonoid G] {p : ℕ} (hp : Prime p) : ∃ (g : G), addOrderOf g = p ^ (AddMonoid.exponent G).factorization p

theorem Commute.orderOf_mul_pow_eq_lcm {G : Type u} [Monoid G] {x y : G} (h : Commute x y) (hx : orderOf x ≠ 0) (hy : orderOf y ≠ 0) : orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)) * y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) = (orderOf x).lcm (orderOf y)

If two commuting elements x and y of a monoid have order n and m, there is an element of order lcm n m. The result actually gives an explicit (computable) element, written as the product of a power of x and a power of y. See also the result below if you don't need the explicit formula.

theorem AddCommute.addOrderOf_add_nsmul_eq_lcm {G : Type u} [AddMonoid G] {x y : G} (h : AddCommute x y) (hx : addOrderOf x ≠ 0) (hy : addOrderOf y ≠ 0) : addOrderOf ((addOrderOf x / (addOrderOf x).factorizationLCMLeft (addOrderOf y)) • x + (addOrderOf y / (addOrderOf x).factorizationLCMRight (addOrderOf y)) • y) = (addOrderOf x).lcm (addOrderOf y)

If two commuting elements x and y of an additive monoid have order n and m, there is an element of order lcm n m. The result actually gives an explicit (computable) element, written as the sum of a multiple of x and a multiple of y. See also the result below if you don't need the explicit formula.

theorem Commute.exists_orderOf_eq_lcm (G : Type u) [Monoid G] {x y : G} (h : Commute x y) : ∃ z ∈ Submonoid.closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)

If two commuting elements x and y of a monoid have order n and m, then there is an element of order lcm n m that lies in the subgroup generated by x and y.

theorem AddCommute.exists_addOrderOf_eq_lcm (G : Type u) [AddMonoid G] {x y : G} (h : AddCommute x y) : ∃ z ∈ AddSubmonoid.closure {x, y}, addOrderOf z = (addOrderOf x).lcm (addOrderOf y)

If two commuting elements x and y of an additive monoid have order n and m, then there is an element of order lcm n m that lies in the additive subgroup generated by x and y.

theorem Monoid.exponent_eq_prime_iff {G : Type u_1} [Monoid G] [Nontrivial G] {p : ℕ} (hp : Nat.Prime p) : exponent G = p ↔ ∀ (g : G), g ≠ 1 → orderOf g = p

A nontrivial monoid has prime exponent p if and only if every non-identity element has order p.

theorem AddMonoid.exponent_eq_prime_iff {G : Type u_1} [AddMonoid G] [Nontrivial G] {p : ℕ} (hp : Nat.Prime p) : exponent G = p ↔ ∀ (g : G), g ≠ 0 → addOrderOf g = p

theorem Monoid.exponent_ne_zero_iff_range_orderOf_finite {G : Type u} [Monoid G] (h : ∀ (g : G), 0 < orderOf g) : exponent G ≠ 0 ↔ (Set.range orderOf).Finite

theorem AddMonoid.exponent_ne_zero_iff_range_addOrderOf_finite {G : Type u} [AddMonoid G] (h : ∀ (g : G), 0 < addOrderOf g) : exponent G ≠ 0 ↔ (Set.range addOrderOf).Finite

theorem Monoid.exponent_eq_zero_iff_range_orderOf_infinite {G : Type u} [Monoid G] (h : ∀ (g : G), 0 < orderOf g) : exponent G = 0 ↔ (Set.range orderOf).Infinite

theorem AddMonoid.exponent_eq_zero_iff_range_addOrderOf_infinite {G : Type u} [AddMonoid G] (h : ∀ (g : G), 0 < addOrderOf g) : exponent G = 0 ↔ (Set.range addOrderOf).Infinite

theorem Monoid.lcm_orderOf_eq_exponent {G : Type u} [Monoid G] [Fintype G] : Finset.univ.lcm orderOf = exponent G

theorem AddMonoid.lcm_addOrderOf_eq_exponent {G : Type u} [AddMonoid G] [Fintype G] : Finset.univ.lcm addOrderOf = exponent G

theorem Monoid.exponent_dvd_of_monoidHom {G : Type u} [Monoid G] {H : Type u_1} [Monoid H] (e : G →* H) (e_inj : Function.Injective ⇑e) : exponent G ∣ exponent H

If there exists an injective, multiplication-preserving map from G to H, then the exponent of G divides the exponent of H.

theorem AddMonoid.exponent_dvd_of_addMonoidHom {G : Type u} [AddMonoid G] {H : Type u_1} [AddMonoid H] (e : G →+ H) (e_inj : Function.Injective ⇑e) : exponent G ∣ exponent H

If there exists an injective, addition-preserving map from G to H, then the exponent of G divides the exponent of H.

theorem Monoid.exponent_eq_of_mulEquiv {G : Type u} [Monoid G] {H : Type u_1} [Monoid H] (e : G ≃* H) : exponent G = exponent H

If there exists a multiplication-preserving equivalence between G and H, then the exponent of G is equal to the exponent of H.

theorem AddMonoid.exponent_eq_of_addEquiv {G : Type u} [AddMonoid G] {H : Type u_1} [AddMonoid H] (e : G ≃+ H) : exponent G = exponent H

If there exists a addition-preserving equivalence between G and H, then the exponent of G is equal to the exponent of H.

@[simp]

theorem Submonoid.exponent_top (G : Type u) [Monoid G] : Monoid.exponent ↥⊤ = Monoid.exponent G

@[simp]

theorem AddSubmonoid.exponent_top (G : Type u) [AddMonoid G] : AddMonoid.exponent ↥⊤ = AddMonoid.exponent G

theorem Submonoid.pow_exponent_eq_one {G : Type u} [Monoid G] {S : Submonoid G} {g : G} (g_in_s : g ∈ S) : g ^ Monoid.exponent ↥S = 1

theorem AddSubmonoid.nsmul_exponent_eq_zero {G : Type u} [AddMonoid G] {S : AddSubmonoid G} {g : G} (g_in_s : g ∈ S) : AddMonoid.exponent ↥S • g = 0

theorem Monoid.ExponentExists.of_finite {G : Type u} [LeftCancelMonoid G] [Finite G] : ExponentExists G

theorem AddMonoid.ExponentExists.of_finite {G : Type u} [AddLeftCancelMonoid G] [Finite G] : ExponentExists G

theorem Monoid.exponent_ne_zero_of_finite {G : Type u} [LeftCancelMonoid G] [Finite G] : exponent G ≠ 0

theorem AddMonoid.exponent_ne_zero_of_finite {G : Type u} [AddLeftCancelMonoid G] [Finite G] : exponent G ≠ 0

theorem Monoid.one_lt_exponent {G : Type u} [LeftCancelMonoid G] [Finite G] [Nontrivial G] : 1 < exponent G

theorem AddMonoid.one_lt_exponent {G : Type u} [AddLeftCancelMonoid G] [Finite G] [Nontrivial G] : 1 < exponent G

instance Monoid.neZero_exponent_of_finite {G : Type u} [LeftCancelMonoid G] [Finite G] : NeZero (exponent G)

instance AddMonoid.neZero_exponent_of_finite {G : Type u} [AddLeftCancelMonoid G] [Finite G] : NeZero (exponent G)

theorem Monoid.exists_orderOf_eq_exponent {G : Type u} [CommMonoid G] (hG : ExponentExists G) : ∃ (g : G), orderOf g = exponent G

theorem AddMonoid.exists_addOrderOf_eq_exponent {G : Type u} [AddCommMonoid G] (hG : ExponentExists G) : ∃ (g : G), addOrderOf g = exponent G

theorem Monoid.exponent_eq_iSup_orderOf {G : Type u} [CommMonoid G] (h : ∀ (g : G), 0 < orderOf g) : exponent G = ⨆ (g : G), orderOf g

theorem AddMonoid.exponent_eq_iSup_addOrderOf {G : Type u} [AddCommMonoid G] (h : ∀ (g : G), 0 < addOrderOf g) : exponent G = ⨆ (g : G), addOrderOf g

theorem Monoid.exponent_eq_iSup_orderOf' {G : Type u} [CommMonoid G] : exponent G = if ∃ (g : G), orderOf g = 0 then 0 else ⨆ (g : G), orderOf g

theorem AddMonoid.exponent_eq_iSup_addOrderOf' {G : Type u} [AddCommMonoid G] : exponent G = if ∃ (g : G), addOrderOf g = 0 then 0 else ⨆ (g : G), addOrderOf g

theorem Monoid.exponent_eq_max'_orderOf {G : Type u} [CancelCommMonoid G] [Fintype G] : exponent G = (Finset.image orderOf Finset.univ).max' ⋯

theorem AddMonoid.exponent_eq_max'_addOrderOf {G : Type u} [AddCancelCommMonoid G] [Fintype G] : exponent G = (Finset.image addOrderOf Finset.univ).max' ⋯

theorem Group.exponent_dvd_card {G : Type u} [Group G] [Fintype G] : Monoid.exponent G ∣ Fintype.card G

theorem AddGroup.exponent_dvd_card {G : Type u} [AddGroup G] [Fintype G] : AddMonoid.exponent G ∣ Fintype.card G

theorem Group.exponent_dvd_nat_card {G : Type u} [Group G] : Monoid.exponent G ∣ Nat.card G

theorem AddGroup.exponent_dvd_nat_card {G : Type u} [AddGroup G] : AddMonoid.exponent G ∣ Nat.card G

theorem Subgroup.exponent_toSubmonoid {G : Type u} [Group G] (H : Subgroup G) : Monoid.exponent ↥H.toSubmonoid = Monoid.exponent ↥H

theorem AddSubgroup.exponent_toAddSubmonoid {G : Type u} [AddGroup G] (H : AddSubgroup G) : AddMonoid.exponent ↥H.toAddSubmonoid = AddMonoid.exponent ↥H

@[simp]

theorem Subgroup.exponent_top {G : Type u} [Group G] : Monoid.exponent ↥⊤ = Monoid.exponent G

@[simp]

theorem AddSubgroup.exponent_top {G : Type u} [AddGroup G] : AddMonoid.exponent ↥⊤ = AddMonoid.exponent G

theorem Subgroup.pow_exponent_eq_one {G : Type u} [Group G] {H : Subgroup G} {g : G} (g_in_H : g ∈ H) : g ^ Monoid.exponent ↥H = 1

theorem AddSubgroup.nsmul_exponent_eq_zero {G : Type u} [AddGroup G] {H : AddSubgroup G} {g : G} (g_in_H : g ∈ H) : AddMonoid.exponent ↥H • g = 0

theorem Group.exponent_dvd_iff_forall_zpow_eq_one {G : Type u} [Group G] {n : ℤ} : ↑(Monoid.exponent G) ∣ n ↔ ∀ (g : G), g ^ n = 1

theorem AddGroup.exponent_dvd_iff_forall_zsmul_eq_zero {G : Type u} [AddGroup G] {n : ℤ} : ↑(AddMonoid.exponent G) ∣ n ↔ ∀ (g : G), n • g = 0

theorem Group.exponent_dvd_sub_iff_zpow_eq_zpow {G : Type u} [Group G] {n m : ℤ} : ↑(Monoid.exponent G) ∣ n - m ↔ ∀ (g : G), g ^ n = g ^ m

theorem AddGroup.exponent_dvd_sub_iff_zsmul_eq_zsmul {G : Type u} [AddGroup G] {n m : ℤ} : ↑(AddMonoid.exponent G) ∣ n - m ↔ ∀ (g : G), n • g = m • g

theorem Monoid.exponent_pi_eq_zero {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → Monoid (M i)] {j : ι} (hj : exponent (M j) = 0) : exponent ((i : ι) → M i) = 0

theorem AddMonoid.exponent_pi_eq_zero {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → AddMonoid (M i)] {j : ι} (hj : exponent (M j) = 0) : exponent ((i : ι) → M i) = 0

theorem MonoidHom.exponent_dvd {F : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [Monoid M₁] [Monoid M₂] [FunLike F M₁ M₂] [MonoidHomClass F M₁ M₂] {f : F} (hf : Function.Surjective ⇑f) : Monoid.exponent M₂ ∣ Monoid.exponent M₁

If f : M₁ →⋆ M₂ is surjective, then the exponent of M₂ divides the exponent of M₁.

theorem AddMonoidHom.exponent_dvd {F : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [AddMonoid M₁] [AddMonoid M₂] [FunLike F M₁ M₂] [AddMonoidHomClass F M₁ M₂] {f : F} (hf : Function.Surjective ⇑f) : AddMonoid.exponent M₂ ∣ AddMonoid.exponent M₁

theorem Monoid.exponent_pi {ι : Type u_1} [Fintype ι] {M : ι → Type u_2} [(i : ι) → Monoid (M i)] : exponent ((i : ι) → M i) = Finset.univ.lcm fun (x : ι) => exponent (M x)

The exponent of finite product of monoids is the Finset.lcm of the exponents of the constituent monoids.

theorem AddMonoid.exponent_pi {ι : Type u_1} [Fintype ι] {M : ι → Type u_2} [(i : ι) → AddMonoid (M i)] : exponent ((i : ι) → M i) = Finset.univ.lcm fun (x : ι) => exponent (M x)

The exponent of finite product of additive monoids is the Finset.lcm of the exponents of the constituent additive monoids.

theorem Monoid.exponent_prod {M₁ : Type u_1} {M₂ : Type u_2} [Monoid M₁] [Monoid M₂] : exponent (M₁ × M₂) = lcm (exponent M₁) (exponent M₂)

The exponent of product of two monoids is the lcm of the exponents of the individuaul monoids.

theorem AddMonoid.exponent_prod {M₁ : Type u_1} {M₂ : Type u_2} [AddMonoid M₁] [AddMonoid M₂] : exponent (M₁ × M₂) = lcm (exponent M₁) (exponent M₂)

The exponent of product of two additive monoids is the lcm of the exponents of the individuaul additive monoids.

Properties of monoids with exponent two

theorem orderOf_eq_two_iff {G : Type u} [Monoid G] (hG : Monoid.exponent G = 2) {x : G} : orderOf x = 2 ↔ x ≠ 1

theorem addOrderOf_eq_two_iff {G : Type u} [AddMonoid G] (hG : AddMonoid.exponent G = 2) {x : G} : addOrderOf x = 2 ↔ x ≠ 0

theorem Commute.of_orderOf_dvd_two {G : Type u} [Monoid G] [IsCancelMul G] (h : ∀ (g : G), orderOf g ∣ 2) (a b : G) : Commute a b

theorem AddCommute.of_addOrderOf_dvd_two {G : Type u} [AddMonoid G] [IsCancelAdd G] (h : ∀ (g : G), addOrderOf g ∣ 2) (a b : G) : AddCommute a b

theorem mul_comm_of_exponent_two {G : Type u} [Monoid G] [IsCancelMul G] (hG : Monoid.exponent G = 2) (a b : G) : a * b = b * a

In a cancellative monoid of exponent two, all elements commute.

theorem add_comm_of_exponent_two {G : Type u} [AddMonoid G] [IsCancelAdd G] (hG : AddMonoid.exponent G = 2) (a b : G) : a + b = b + a

@[reducible, inline]

abbrev commMonoidOfExponentTwo {G : Type u} [Monoid G] [IsCancelMul G] (hG : Monoid.exponent G = 2) : CommMonoid G

Any cancellative monoid of exponent two is abelian.

Equations

• commMonoidOfExponentTwo hG = { toMonoid := inst✝¹, mul_comm := ⋯ }

@[reducible, inline]

abbrev addCommMonoidOfExponentTwo {G : Type u} [AddMonoid G] [IsCancelAdd G] (hG : AddMonoid.exponent G = 2) : AddCommMonoid G

Any additive group of exponent two is abelian.

Equations

• addCommMonoidOfExponentTwo hG = { toAddMonoid := inst✝¹, add_comm := ⋯ }

theorem inv_eq_self_of_exponent_two {G : Type u} [Group G] (hG : Monoid.exponent G = 2) (x : G) : x⁻¹ = x

In a group of exponent two, every element is its own inverse.

theorem neg_eq_self_of_exponent_two {G : Type u} [AddGroup G] (hG : AddMonoid.exponent G = 2) (x : G) : -x = x

theorem inv_eq_self_of_orderOf_eq_two {G : Type u} [Group G] {x : G} (hx : orderOf x = 2) : x⁻¹ = x

If an element in a group has order two, then it is its own inverse.

theorem neg_eq_self_of_addOrderOf_eq_two {G : Type u} [AddGroup G] {x : G} (hx : addOrderOf x = 2) : -x = x

theorem mul_not_mem_of_orderOf_eq_two {G : Type u} [Group G] {x y : G} (hx : orderOf x = 2) (hy : orderOf y = 2) (hxy : x ≠ y) : x * y ∉ {x, y, 1}

theorem add_not_mem_of_addOrderOf_eq_two {G : Type u} [AddGroup G] {x y : G} (hx : addOrderOf x = 2) (hy : addOrderOf y = 2) (hxy : x ≠ y) : x + y ∉ {x, y, 0}

theorem mul_not_mem_of_exponent_two {G : Type u} [Group G] (h : Monoid.exponent G = 2) {x y : G} (hx : x ≠ 1) (hy : y ≠ 1) (hxy : x ≠ y) : x * y ∉ {x, y, 1}

theorem add_not_mem_of_exponent_two {G : Type u} [AddGroup G] (h : AddMonoid.exponent G = 2) {x y : G} (hx : x ≠ 0) (hy : y ≠ 0) (hxy : x ≠ y) : x + y ∉ {x, y, 0}