mathlib documentation

algebra.group.conj

Conjugacy of group elements

def is_conj {α : Type u} [group α] :
α → α → Prop

We say that a is conjugate to b if for some c we have c * a * c⁻¹ = b.

Equations
theorem is_conj_refl {α : Type u} [group α] (a : α) :

theorem is_conj_symm {α : Type u} [group α] {a b : α} :
is_conj a bis_conj b a

theorem is_conj_trans {α : Type u} [group α] {a b c : α} :
is_conj a bis_conj b cis_conj a c

@[simp]
theorem is_conj_one_right {α : Type u} [group α] {a : α} :
is_conj 1 a a = 1

@[simp]
theorem is_conj_one_left {α : Type u} [group α] {a : α} :
is_conj a 1 a = 1

@[simp]
theorem conj_inv {α : Type u} [group α] {a b : α} :
((b * a) * b⁻¹)⁻¹ = (b * a⁻¹) * b⁻¹

@[simp]
theorem conj_mul {α : Type u} [group α] {a b c : α} :
((b * a) * b⁻¹) * (b * c) * b⁻¹ = (b * a * c) * b⁻¹

@[simp]
theorem is_conj_iff_eq {α : Type u_1} [comm_group α] {a b : α} :
is_conj a b a = b

theorem monoid_hom.map_is_conj {α : Type u} {β : Type v} [group α] [group β] (f : α →* β) {a b : α} :
is_conj a bis_conj (f a) (f b)