norm_cast_rat

Mathlib.Analysis.Normed.Group.Rat

URI: https://scilib.ai/kg/mathlib#Int.norm_cast_rat

English

The norm of an integer cast to rationals equals the integer's norm.

Русский

Норма целого, приведённого к ℚ, равна норме самого целого.

LaTeX

$$‖(m : ℚ)‖ = ‖m‖ for m ∈ ℤ$$

Lean4

@[norm_cast, simp]
theorem _root_.Int.norm_cast_rat (m : ℤ) : ‖(m : ℚ)‖ = ‖m‖ := by rw [← Rat.norm_cast_real, ← Int.norm_cast_real];
  congr 1

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

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

Разделы

Аффилиация

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