instNormMulClass

Mathlib.NumberTheory.Padics.PadicIntegers

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

English

The norm on Z_p is multiplicative: for any a,b in Z_p, ||a b|| = ||a|| · ||b||.

Русский

Норма на Z_p умножаема: для любых a,b в Z_p выполняется ||a b|| = ||a|| · ||b||.

LaTeX

$$$$\|ab\| = \|a\|\|b\|.$$$$

Lean4

instance : NormMulClass ℤ_[p] :=
  ⟨fun x y ↦ by simp [norm_def]⟩

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

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

Разделы

Аффилиация

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