norm_intCast_abs

Mathlib.Analysis.Normed.Ring.Basic

URI: https://scilib.ai/kg/mathlib#norm_intCast_abs

English

The norm of the absolute value of an integer, cast into α, equals the norm of the integer cast into α.

Русский

Норма модуля целого числа, приведённого к α, равна норме самого числа в α.

LaTeX

$$$\|(|z| : \mathbb{Z}) : \alpha|\| = \|z : \alpha\|$$$

Lean4

@[simp]
theorem norm_intCast_abs (z : ℤ) : ‖((|z| : ℤ) : α)‖ = ‖(z : α)‖ := by simp [← norm_natAbs]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru