arg_eq_arg

Mathlib.Analysis.SpecialFunctions.Complex.Circle

URI: https://scilib.ai/kg/mathlib#Circle.arg_eq_arg

English

For two points on the circle, arg z = arg w if and only if z = w.

Русский

Для двух точек на окружности arg z = arg w тогда и только тогда, когда z = w.

LaTeX

$$$$\\forall \\{z,w\\} \\in \\ Circle: \\.arg z = \\arg w \\iff z = w.$$$$

Lean4

@[simp]
theorem arg_eq_arg {z w : Circle} : arg z = arg w ↔ z = w :=
  injective_arg.eq_iff

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

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

Разделы

Аффилиация

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