isometry_intCast — Mathlib

English

The canonical embedding of integers into ℂ, n ↦ n, is distance-preserving: Int.cast is an isometry.

Русский

Каноническое вложение целых в ℂ, n ↦ n, сохраняет расстояние: Int.cast является изометрией.

LaTeX

$$$\\\\text{Isometry} (\\\\text{Int.cast})$$$

Lean4

theorem isometry_intCast : Isometry ((↑) : ℤ → ℂ) :=
  Isometry.of_dist_eq <| by
    simp_rw [← Complex.ofReal_intCast, Complex.isometry_ofReal.dist_eq, Int.dist_cast_real, implies_true]

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