norm_def

Mathlib.NumberTheory.Padics.Complex

URI: https://scilib.ai/kg/mathlib#PadicComplex.norm_def

English

The norm on ℂ_p equals the extended Valued.norm from PadicComplex valuation.

Русский

Норма на ℂ_p совпадает с нормой, выходящей из реализованной оценки.

LaTeX

$$$\mathrm{Norm}_{\mathbb{C}_p} = \mathrm{Valued}.\mathrm{norm}$$$

Lean4

theorem norm_def : (Norm.norm : ℂ_[p] → ℝ) = Valued.norm :=
  rfl

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

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

Разделы

Аффилиация

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