ofNat_re

Mathlib.Analysis.RCLike.Basic

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

English

For every n ≥ 2, the real part of ofNat(n) in K equals ofNat(n).

Русский

Пусть n ≥ 2. Действительная часть ofNat(n) в K равна ofNat(n).

LaTeX

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

Lean4

@[simp, rclike_simps]
theorem ofNat_re (n : ℕ) [n.AtLeastTwo] : re (ofNat(n) : K) = ofNat(n) :=
  natCast_re n

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

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

Разделы

Аффилиация

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