mathlib docs: algebra.group.conj

def is_conj {α : Type u} [group α] (a b : α) :

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 : α} (a_1 : is_conj a b) :

theorem is_conj_trans {α : Type u} [group α] {a b c : α} (a_1 : is_conj a b) (a_2 : is_conj b c) :

@[simp]

theorem is_conj_one_right {α : Type u} [group α] {a : α} :

@[simp]

theorem is_conj_one_left {α : Type u} [group α] {a : α} :

@[simp]

theorem conj_inv {α : Type u} [group α] {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 : α} :

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

mathlib documentation