English
Conjugacy is the equivalence relation on a monoid: two elements are conjugate if there exists a unit u with u x = y u; this relation is reflexive, symmetric, and transitive.
Русский
Сопряжённость является отношением эквивалентности на моидe: два элемента сопряжены, если существует единица u такая, что u x = y u; это отношение рефлексивно, симметрично и транзитивно.
LaTeX
$$$\text{IsConj is an equivalence relation on }\alpha\ (i.e.,\ \forall x\, IsConj(x,x),\ \forall x,y\ IsConj(x,y)\Rightarrow IsConj(y,x),\ \forall x,y,z\ IsConj(x,y)\land IsConj(y,z)\Rightarrow IsConj(x,z))$$$
Lean4
/-- The setoid of the relation `IsConj` iff there is a unit `u` such that `u * x = y * u` -/
protected def setoid (α : Type*) [Monoid α] : Setoid α
where
r := IsConj
iseqv := ⟨IsConj.refl, IsConj.symm, IsConj.trans⟩
