instNormedAddCommGroup

Mathlib.Analysis.Normed.Group.Rat

URI: https://scilib.ai/kg/mathlib#Rat.instNormedAddCommGroup

← MathLib Explorer

English

The rationals ℚ form a NormedAddCommGroup with norm |r| when viewed as a subset of ℝ.

Русский

числа Q образуют NormedAddCommGroup, нормa равна модулю числа, при естественном включении в ℝ.

LaTeX

$$NormedAddCommGroup(ℚ)$$

Lean4

instance instNormedAddCommGroup : NormedAddCommGroup ℚ
    where
  norm r := ‖(r : ℝ)‖
  dist_eq r₁ r₂ := by simp only [Rat.dist_eq, norm, Rat.cast_sub]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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