natCast_natAbs_norm — Mathlib

English

For any type α with AddGroupWithOne, and any Gaussian integer x, the natAbs of the norm, viewed in α, equals the norm.

Русский

Для любого типа α с AddGroupWithOne и любого x ∈ ℤ[i], natAbs нормы, приведенная к α, равна норме.

LaTeX

$$$ \forall {\alpha} [AddGroupWithOne \alpha] (x : \mathbb{Z}[i]), (x.norm.natAbs : \alpha) = x.norm $$$

Lean4

theorem natCast_natAbs_norm {α : Type*} [AddGroupWithOne α] (x : ℤ[i]) : (x.norm.natAbs : α) = x.norm := by simp

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