norm_intCast_eq_abs_mul_norm_one — Mathlib

English

For a ∈ ℤ mapped to α (SeminormedRing α) with NormSMulClass ℤ α, we have ‖a‖ = |a| · ‖1‖.

Русский

Для целого a, отображённого как целая константа в нормированном кольце α, выполняется ‖a‖ = |a| · ‖1‖.

LaTeX

$$$\\|a\\| = |a| \\cdot \\|1_{\\alpha}\\|$$$

Lean4

theorem norm_intCast_eq_abs_mul_norm_one (α) [SeminormedRing α] [NormSMulClass ℤ α] (n : ℤ) :
    ‖(n : α)‖ = |n| * ‖(1 : α)‖ := by rw [← zsmul_one, norm_smul, Int.norm_eq_abs, Int.cast_abs]

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