addVal_uniformizer

Mathlib.RingTheory.DiscreteValuationRing.Basic

URI: https://scilib.ai/kg/mathlib#IsDiscreteValuationRing.addVal_uniformizer

← MathLib Explorer

English

If ϖ is an irreducible element, then addVal(ϖ) = 1.

Русский

Если ϖ ирредуцируем, то addVal(ϖ) = 1.

LaTeX

$$$\mathrm{addVal}(\varpi) = 1$$$

Lean4

@[simp]
theorem addVal_uniformizer {ϖ : R} (hϖ : Irreducible ϖ) : addVal R ϖ = 1 := by
  simpa only [one_mul, eq_self_iff_true, Units.val_one, pow_one, forall_true_left, Nat.cast_one] using
    addVal_def ϖ 1 hϖ 1

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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