ofReal_ofNat — Mathlib

English

For every n ≥ 2, the embedded value obtained by first embedding n into ℝ and then into K equals the direct nat cast into K.

Русский

Для каждого n ≥ 2, образ из n в ℝ затем в K совпадает с прямым приведением n в K.

LaTeX

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

Lean4

@[rclike_simps, norm_cast]
theorem ofReal_ofNat (n : ℕ) [n.AtLeastTwo] : ((ofNat(n) : ℝ) : K) = ofNat(n) :=
  ofReal_natCast n

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