Basic ordered group facts

This file proves some basic facts about ordered groups.

theorem pnat_pow_eq_nat_pow {α : Type u} [Group α] (x : α) (n : ℕ+) : x ^ ↑n = x ^ n

theorem split_first_and_last_factor_of_product_group {α : Type u} [Group α] {a b : α} {n : ℕ} : (a * b) ^ (n + 1) = a * (b * a) ^ n * b

theorem pos_exp_pos_pos {α : Type u} [LeftOrderedGroup α] {x : α} (pos_x : 1 < x) {z : ℤ} (pos_z : z > 0) : 1 < x ^ z

theorem nonneg_exp_pos_nonneg {α : Type u} [LeftOrderedGroup α] {x : α} (pos_x : 1 < x) {z : ℤ} (pos_z : z ≥ 0) : 1 ≤ x ^ z

theorem pos_exp_neg_neg {α : Type u} [LeftOrderedGroup α] {x : α} (neg_x : x < 1) {z : ℤ} (pos_z : z > 0) : x ^ z < 1

theorem neg_exp_pos_neg {α : Type u} [LeftOrderedGroup α] {x : α} (pos_x : 1 < x) {z : ℤ} (neg_z : z < 0) : x ^ z < 1

theorem neg_exp_neg_pos {α : Type u} [LeftOrderedGroup α] {x : α} (neg_x : x < 1) {z : ℤ} (neg_z : z < 0) : 1 < x ^ z

theorem pos_arch {α : Type u} [LeftOrderedGroup α] {x y : α} (pos_x : 1 < x) (pos_y : 1 < y) (z : ℤ) : x ^ z > y → z > 0

theorem pos_lt_exp_lt {α : Type u} [LeftOrderedGroup α] {f : α} (f_pos : 1 < f) {a b : ℤ} (f_lt : f ^ a < f ^ b) : a < b

instance instLeftOrderedSemigroup {α : Type u} [LeftOrderedGroup α] : LeftOrderedSemigroup α

Equations

• instLeftOrderedSemigroup = { toSemigroup' := instSemigroup'OfSemigroup, toPartialOrder := LeftOrderedGroup.toPartialOrder, mul_le_mul_left := ⋯ }

theorem pos_neg_disjoint {α : Type u} [LeftOrderedGroup α] : Disjoint ↑(PositiveCone α) ↑(NegativeCone α)

def normal_semigroup {α : Type u} [Group α] (x : Subsemigroup α) : Prop

Equations

• normal_semigroup x = ∀ (s : ↥x) (g : α), g * ↑s * g⁻¹ ∈ x

def pos_normal_ordered {α : Type u} [LeftOrderedGroup α] (pos_normal : normal_semigroup (PositiveCone α)) (a b : α) : a ≤ b → ∀ (c : α), a * c ≤ b * c

A left ordered group whose positive cone is a normal semigroup is an ordered group.

Equations

• ⋯ = ⋯

theorem comm_factor_le_group {α : Type u} [LinearOrderedGroup α] {a b : α} (h : a * b ≤ b * a) (n : ℕ) : a ^ n * b ^ n ≤ (a * b) ^ n

theorem comm_swap_le_group {α : Type u} [LinearOrderedGroup α] {a b : α} (h : a * b ≤ b * a) (n : ℕ) : (a * b) ^ n ≤ (b * a) ^ n

theorem comm_dist_le_group {α : Type u} [LinearOrderedGroup α] {a b : α} (h : a * b ≤ b * a) (n : ℕ) : (b * a) ^ n ≤ b ^ n * a ^ n

theorem pos_exp_lt_lt {α : Type u} [LinearOrderedGroup α] {f : α} (f_pos : 1 < f) {a b : ℤ} (a_lt_b : a < b) : f ^ a < f ^ b

theorem pos_exp_le_le {α : Type u} [LinearOrderedGroup α] {f : α} (f_pos : 1 < f) {a b : ℤ} (a_le_b : a ≤ b) : f ^ a ≤ f ^ b