English
If K is a field and hg1, hg_k, hg_pm are as above, then the value of the RingNorm constructed from normFromConst at x equals the value of seminormFromConst' at x: normFromConst hg1 hg_k hg_pm x = seminormFromConst' hg1 hg_k hg_pm x.
Русский
Пусть K — поле и hg1, hg_k, hg_pm таковы же; тогда нормa из normFromConst на x совпадает со значением seminormFromConst' на x: normFromConst hg1 hg_k hg_pm x = seminormFromConst' hg1 hg_k hg_pm x.
LaTeX
$$$\mathrm{normFromConst}\; hg1\; hg_k\; hg_pm\; x = \operatorname{seminormFromConst'}_{hg1 hg_k hg_pm}(x)$$$
Lean4
/-- If `K` is a field, the function `seminormFromConst` is a `RingNorm` on `K`. -/
def normFromConst {k : K} {g : RingSeminorm K} (hg1 : g 1 ≤ 1) (hg_k : g k ≠ 0) (hg_pm : IsPowMul g) : RingNorm K :=
(seminormFromConst hg1 hg_k hg_pm).toRingNorm
(RingSeminorm.ne_zero_iff.mpr ⟨k, by simpa [seminormFromConst_def, seminormFromConst_apply_c] using hg_k⟩)
