English
In Monoid M, SemiconjBy (a : M) x y for Units M is equivalent to SemiconjBy a x y; i.e., a semiconjugates x to y as a unit iff it does so in M.
Русский
В моноиде M полусопряжение SemiconjBy (a : M) x y для Units M эквивалентно SemiconjBy a x y; т.е. полусопряжение сохраняется в единицах и в M.
LaTeX
$$$$\forall a,x,y:\ SemiconjBy (a : M) x y \iff SemiconjBy a x y.$$$$
Lean4
@[to_additive (attr := simp)]
theorem units_val_iff {a x y : Mˣ} : SemiconjBy (a : M) x y ↔ SemiconjBy a x y :=
⟨units_of_val, units_val⟩