instCircularOrder

Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

URI: https://scilib.ai/kg/mathlib#Real.Angle.instCircularOrder

English

The type Real.Angle carries a circular order, i.e., a natural cyclic comparison of angles modulo 2π.

Русский

У Real.Angle имеется циклический порядок, соответствующий углам по модулю 2π.

LaTeX

$$$$ \text{Real.Angle} \text{ has a circular order.} $$$$

Lean4

instance : CircularOrder Real.Angle :=
  QuotientAddGroup.circularOrder (hp' := ⟨by simp [pi_pos]⟩)

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

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

Разделы

Аффилиация

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