intNorm_coe — Mathlib

English

The real-valued intNorm of an element in the integerSet equals the norm of its mixedEmbedding image, viewed in Real.

Русский

Число intNorm элемента integerSet(K) равно норме от его изображения в смешанном вложении.

LaTeX

$$intNorm a = (mixedEmbedding(K) a)_norm as Real.$$

Lean4

@[simp]
theorem intNorm_coe (a : integerSet K) : (intNorm a : ℝ) = mixedEmbedding.norm (a : mixedSpace K) := by
  rw [intNorm, Int.cast_natAbs, ← Rat.cast_intCast, Int.cast_abs, Algebra.coe_norm_int, ← norm_eq_norm,
    mixedEmbedding_preimageOfMemIntegerSet]

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