iff_ideal_total

Mathlib.RingTheory.Valuation.ValuationRing

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

← MathLib Explorer

English

ValuationRing R is equivalent to IsTotal (Ideal R) (≤).

Русский

ValuationRing R эквивалентно IsTotal (Ideal R) (≤).

LaTeX

$$$ ValuationRing R \\iff IsTotal(\\mathrm{Ideal} R)(≤)$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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