ofNat_arg

Mathlib.Analysis.SpecialFunctions.Complex.Arg

URI: https://scilib.ai/kg/mathlib#Complex.ofNat_arg

English

For any n with AtLeastTwo, arg(ofNat n) = 0.

Русский

Для любого n, удовлетворяющего AtLeastTwo, arg(ofNat n) = 0.

LaTeX

$$$$ \arg(\operatorname{ofNat}(n)) = 0, \quad \text{если } n \text{ имеет } AtLeastTwo. $$$$

Lean4

@[simp]
theorem ofNat_arg {n : ℕ} [n.AtLeastTwo] : arg ofNat(n) = 0 :=
  natCast_arg

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

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

Разделы

Аффилиация

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