English
The relation “there exists an element that semiconjugates a to b” is reflexive; in particular, using c = 1 shows SemiconjBy 1 a b holds when a = b.
Русский
Отношение «существует c, такое что c полусопрягает a к b» является рефлексивным; в частности c = 1 даёт SemiconjBy 1 a b для a = b.
LaTeX
$$$$\text{Reflexive: } \forall a\in M,\ SemiconjBy 1\ a\ a.$$$$
Lean4
/-- The relation “there exists an element that semiconjugates `a` to `b`” on a monoid (or, more
generally, on `MulOneClass` type) is reflexive. -/
@[to_additive /-- The relation “there exists an element that semiconjugates `a` to `b`” on an
additive monoid (or, more generally, on an `AddZeroClass` type) is reflexive. -/
]
protected theorem reflexive : Reflexive fun a b : M ↦ ∃ c, SemiconjBy c a b
| a => ⟨1, one_left a⟩
