intValuationDef_if_pos

Mathlib.RingTheory.DedekindDomain.AdicValuation

URI: https://scilib.ai/kg/mathlib#IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_pos

English

If r = 0, then intValuationDef(r) = 0.

Русский

Если r = 0, то intValuationDef(r) = 0.

LaTeX

$$intValuationDef (r) = 0 if r = 0$$

Lean4

theorem intValuationDef_if_pos {r : R} (hr : r = 0) : v.intValuationDef r = 0 :=
  if_pos hr

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

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

Разделы

Аффилиация

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