semiconjBy_iff_semiconj — Mathlib

English

The map translate: Multiplicative ℝ →* CircleDeg1Liftˣ is a monoid hom sending x to translation by x.

Русский

Отображение translate: Multiplicative ℝ →* CircleDeg1Liftˣ есть моноидный гомоморфизм, сопоставляющий x с трансляцией на x.

LaTeX

$$$\\text{translate} : \\text{Multiplicative }\\mathbb{R} \\to * CircleDeg1Lift^\\times$ is a monoid hom sending $x$ to translation by $x$$$

Lean4

theorem semiconjBy_iff_semiconj {f g₁ g₂ : CircleDeg1Lift} : SemiconjBy f g₁ g₂ ↔ Semiconj f g₁ g₂ :=
  CircleDeg1Lift.ext_iff

Похожие утверждения