instNormMulClass

Mathlib.Analysis.Normed.Ring.Lemmas

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

English

The integers carry a NormMulClass: |ab| ≤ |a||b| (and equality for real norm).

Русский

Целые числа образуют NormMulClass: |ab| ≤ |a||b| (и равенство для вещественной нормы).

LaTeX

$$$ \\text{NormMulClass}(\\mathbb{Z}) \\text{ with } |ab| \\le |a|\\,|b|$.$$

Lean4

instance instNormMulClass : NormMulClass ℤ :=
  ⟨fun a b ↦ by simp [← Int.norm_cast_real, abs_mul]⟩

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

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

Разделы

Аффилиация

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