instNormSMulClassInt

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.instNormSMulClassInt

English

The Z-action on K is norm-preserving: for all r ∈ ℤ and x ∈ K, ‖r x‖ = |r| ‖x‖.

Русский

Действие целых чисел на K сохраняет норму: ∀ r∈ℤ, x∈K, ‖r x‖ = |r|‖x‖.

LaTeX

$$$$ \\| r \\cdot x \\| = |r| \\| x \\| \\quad (r \\in \\mathbb{Z},\\ x \\in K). $$$$

Lean4

instance : NormSMulClass ℤ K where
  norm_smul r x := by rw [zsmul_eq_mul, norm_mul, ← ofReal_intCast, norm_ofReal, Int.norm_eq_abs]

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

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

Разделы

Аффилиация

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