coe_toOrderIso_inv

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

English

For f ∈ CircleDeg1Liftˣ, ⇑(toOrderIso f).symm = f⁻¹.

Русский

Для f ∈ CircleDeg1Liftˣ верно ⇑(toOrderIso f).symm = f⁻¹.

LaTeX

$$$\\text{coe_toOrderIso_symm}(f) = f^{-1}$$$

Lean4

@[simp]
theorem coe_toOrderIso_inv (f : CircleDeg1Liftˣ) : ⇑(toOrderIso f)⁻¹ = (f⁻¹ : CircleDeg1Liftˣ) :=
  rfl

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

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

Разделы

Аффилиация

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