seminormFromConstRingNormOfField_def

English

For a field K and a RingSeminorm g satisfying g(1) ≤ 1 and g(k) ≠ 0 with IsPowMul, the value of the RingNorm associated to normFromConst coincides with seminormFromConst' on any x ∈ K.

Русский

Для поля K и кольцевой семиномормы g с g(1) ≤ 1, g(k) ≠ 0 и IsPowMul выполняется, что норма из normFromConst равна seminormFromConst' на любом x ∈ K.

LaTeX

$$$\mathrm{normFromConst}\; g \, x = \operatorname{seminormFromConst'}_{hg1 hg_k hg_pm}(x)$$$

Lean4

theorem seminormFromConstRingNormOfField_def {k : K} {g : RingSeminorm K} (hg1 : g 1 ≤ 1) (hg_k : g k ≠ 0)
    (hg_pm : IsPowMul g) (x : K) : normFromConst hg1 hg_k hg_pm x = seminormFromConst' hg1 hg_k hg_pm x :=
  rfl

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