translationNumber_conj_eq — Mathlib

English

For f ∈ CircleDeg1Liftˣ and g ∈ CircleDeg1Lift, τ(↑f g ↑f⁻¹) = τ(g).

Русский

Для f ∈ CircleDeg1Liftˣ и g ∈ CircleDeg1Lift, τ( f g f^{-1} ) = τ(g).

LaTeX

$$$ \forall f \in CircleDeg1Lift^{\times}, \forall g \in CircleDeg1Lift, τ( (f) g (f)^{-1} ) = τ(g). $$$

Lean4

@[simp]
theorem translationNumber_conj_eq (f : CircleDeg1Liftˣ) (g : CircleDeg1Lift) : τ (↑f * g * ↑f⁻¹) = τ g :=
  (translationNumber_eq_of_semiconjBy (f.mk_semiconjBy g)).symm

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