translationNumber_units_inv

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

URI: https://scilib.ai/kg/mathlib#CircleDeg1Lift.translationNumber_units_inv

← MathLib Explorer

English

For f a unit in CircleDeg1Lift, τ(f^{-1}) = -τ(f).

Русский

Для f — элемент-подобный единице CircleDeg1Lift, τ(f^{-1}) = -τ(f).

LaTeX

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

Lean4

@[simp]
theorem translationNumber_units_inv (f : CircleDeg1Liftˣ) : τ ↑f⁻¹ = -τ f :=
  eq_neg_iff_add_eq_zero.2 <| by simp [← translationNumber_mul_of_commute (Commute.refl _).units_inv_left]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru