ofNat_im

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.ofNat_im

English

For every n ≥ 2, the imaginary part of ofNat(n) in K is zero.

Русский

Для каждого n ≥ 2 мнимая часть ofNat(n) в K равна нулю.

LaTeX

$$$$\forall n \in \mathbb{N},\ n \ge 2 \Rightarrow \operatorname{Im}(\operatorname{ofNat}(n) : K) = 0.$$$$

Lean4

@[simp, rclike_simps]
theorem ofNat_im (n : ℕ) [n.AtLeastTwo] : im (ofNat(n) : K) = 0 :=
  natCast_im n

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

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

Разделы

Аффилиация

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