norm_natCast — Mathlib

English

Same as norm_natCast, another form; the simp lemma for natural cast preserves the norm.

Русский

То же самое, что norm_natCast, ещё одно представление для сохранения нормы приведением к натуральному.

LaTeX

$$$\\|n\\| = n$$$

Lean4

@[simp]
theorem norm_natCast {α : Type*} [SeminormedRing α] [NormOneClass α] [NormSMulClass ℤ α] (a : ℕ) : ‖(a : α)‖ = a := by
  simpa using norm_natCast_eq_mul_norm_one α a

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