norm_natAbs — Mathlib

English

For any integer z, the norm of its natural absolute value embedded into α equals the norm of z embedded into α.

Русский

Для целого числа z норма |z| в α равна норме z в α.

LaTeX

$$$\|(|z|)^{cast}\| = \|z^{cast}\|$ for all z ∈ ℤ.$$

Lean4

theorem norm_natAbs (z : ℤ) : ‖(z.natAbs : α)‖ = ‖(z : α)‖ :=
  by
  rcases z.natAbs_eq with hz | hz
  · rw [← Int.cast_natCast, ← hz]
  · rw [← Int.cast_natCast, ← norm_neg, ← Int.cast_neg, ← hz]

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