iff_dvd_total

Mathlib.RingTheory.Valuation.ValuationRing

URI: https://scilib.ai/kg/mathlib#ValuationRing.iff_dvd_total

← MathLib Explorer

English

ValuationRing R is equivalent to IsTotal R (x ∣ y).

Русский

ValuationRing R эквивалентно IsTotal R (x ∣ y).

LaTeX

$$$ ValuationRing R \\iff IsTotal R(\\cdot \\mid \\cdot)$$$

Lean4

theorem iff_dvd_total : ValuationRing R ↔ IsTotal R (· ∣ ·) :=
  Iff.trans (⟨fun inst ↦ inst.toPreValuationRing, fun _ ↦ .mk⟩) PreValuationRing.iff_dvd_total

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

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

Разделы

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

Аффилиация

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