norm_natCast

Mathlib.Analysis.RCLike.Basic

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

← MathLib Explorer

English

For every n ∈ ℕ, the norm of n embedded into K equals n.

Русский

Для любого n ∈ ℕ норма n, введённого в K, равна n.

LaTeX

$$$$\| (n : K) \| = n.$$$$

Lean4

@[simp 1100, rclike_simps, norm_cast]
theorem norm_natCast (n : ℕ) : ‖(n : K)‖ = n := by
  rw [← ofReal_natCast]
  exact norm_of_nonneg (Nat.cast_nonneg n)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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